%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SWV533-1.010 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n029.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Wed Jul 20 21:44:00 EDT 2022
% Result : Satisfiable 0.44s 0.60s
% Output : Saturation 0.44s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 1660)
% Comments :
%------------------------------------------------------------------------------
cnf(1708,plain,
( equal(i7,u)
| equal(select(a_1249,u),select(a_1245,u)) ),
inference(rew,[status(thm),theory(equality)],[277,1660]),
[iquote('9:Rew:277.1,1660.1')] ).
cnf(1659,plain,
( equal(i7,u)
| equal(select(a_1286,u),select(a_1284,u)) ),
inference(rew,[status(thm),theory(equality)],[1652,286]),
[iquote('9:Rew:1652.0,286.0')] ).
cnf(1985,plain,
equal(store(a_1300,i7,e_1246),a_1302),
inference(rew,[status(thm),theory(equality)],[1944,788]),
[iquote('9:Rew:1944.0,788.0')] ).
cnf(1984,plain,
equal(store(a_1292,i7,e_1246),a_1294),
inference(rew,[status(thm),theory(equality)],[1944,718]),
[iquote('9:Rew:1944.0,718.0')] ).
cnf(1983,plain,
equal(store(a_1302,i7,e_1246),a_1304),
inference(rew,[status(thm),theory(equality)],[1944,791]),
[iquote('9:Rew:1944.0,791.0')] ).
cnf(1982,plain,
equal(store(a_1306,i7,e_1246),a_1307),
inference(rew,[status(thm),theory(equality)],[1944,792]),
[iquote('9:Rew:1944.0,792.0')] ).
cnf(1981,plain,
equal(store(a_1304,i7,e_1246),a_1306),
inference(rew,[status(thm),theory(equality)],[1944,793]),
[iquote('9:Rew:1944.0,793.0')] ).
cnf(1980,plain,
equal(store(a_1298,i7,e_1246),a_1300),
inference(rew,[status(thm),theory(equality)],[1944,760]),
[iquote('9:Rew:1944.0,760.0')] ).
cnf(1979,plain,
equal(store(a_1294,i7,e_1246),a_1296),
inference(rew,[status(thm),theory(equality)],[1944,764]),
[iquote('9:Rew:1944.0,764.0')] ).
cnf(1978,plain,
equal(store(a_1296,i7,e_1246),a_1298),
inference(rew,[status(thm),theory(equality)],[1944,765]),
[iquote('9:Rew:1944.0,765.0')] ).
cnf(1977,plain,
equal(store(a_1307,i7,e_1246),a_1309),
inference(rew,[status(thm),theory(equality)],[1944,964]),
[iquote('9:Rew:1944.0,964.0')] ).
cnf(1976,plain,
equal(store(a_1309,i7,e_1246),a_1311),
inference(rew,[status(thm),theory(equality)],[1944,971]),
[iquote('9:Rew:1944.0,971.0')] ).
cnf(1975,plain,
equal(store(a_1311,i7,e_1246),a_1313),
inference(rew,[status(thm),theory(equality)],[1944,1028]),
[iquote('9:Rew:1944.0,1028.0')] ).
cnf(1974,plain,
equal(store(a_1317,i7,e_1246),a_1319),
inference(rew,[status(thm),theory(equality)],[1944,1033]),
[iquote('9:Rew:1944.0,1033.0')] ).
cnf(1973,plain,
equal(store(a_1315,i7,e_1246),a_1317),
inference(rew,[status(thm),theory(equality)],[1944,1037]),
[iquote('9:Rew:1944.0,1037.0')] ).
cnf(1972,plain,
equal(store(a_1313,i7,e_1246),a_1315),
inference(rew,[status(thm),theory(equality)],[1944,1038]),
[iquote('9:Rew:1944.0,1038.0')] ).
cnf(1970,plain,
equal(select(a_1302,i7),e_1246),
inference(rew,[status(thm),theory(equality)],[1944,769]),
[iquote('9:Rew:1944.0,769.0')] ).
cnf(1969,plain,
equal(select(a_1294,i7),e_1246),
inference(rew,[status(thm),theory(equality)],[1944,708]),
[iquote('9:Rew:1944.0,708.0')] ).
cnf(1968,plain,
equal(select(a_1304,i7),e_1246),
inference(rew,[status(thm),theory(equality)],[1944,772]),
[iquote('9:Rew:1944.0,772.0')] ).
cnf(1971,plain,
equal(select(a_1292,i7),e_1246),
inference(rew,[status(thm),theory(equality)],[1944,373]),
[iquote('9:Rew:1944.0,373.0')] ).
cnf(1967,plain,
equal(select(a_1306,i7),e_1246),
inference(rew,[status(thm),theory(equality)],[1944,778]),
[iquote('9:Rew:1944.0,778.0')] ).
cnf(1966,plain,
equal(select(a_1300,i7),e_1246),
inference(rew,[status(thm),theory(equality)],[1944,759]),
[iquote('9:Rew:1944.0,759.0')] ).
cnf(1965,plain,
equal(select(a_1298,i7),e_1246),
inference(rew,[status(thm),theory(equality)],[1944,763]),
[iquote('9:Rew:1944.0,763.0')] ).
cnf(1964,plain,
equal(select(a_1296,i7),e_1246),
inference(rew,[status(thm),theory(equality)],[1944,762]),
[iquote('9:Rew:1944.0,762.0')] ).
cnf(1963,plain,
equal(select(a_1307,i7),e_1246),
inference(rew,[status(thm),theory(equality)],[1944,777]),
[iquote('9:Rew:1944.0,777.0')] ).
cnf(1962,plain,
equal(select(a_1309,i7),e_1246),
inference(rew,[status(thm),theory(equality)],[1944,962]),
[iquote('9:Rew:1944.0,962.0')] ).
cnf(1961,plain,
equal(select(a_1311,i7),e_1246),
inference(rew,[status(thm),theory(equality)],[1944,970]),
[iquote('9:Rew:1944.0,970.0')] ).
cnf(1960,plain,
equal(select(a_1313,i7),e_1246),
inference(rew,[status(thm),theory(equality)],[1944,1026]),
[iquote('9:Rew:1944.0,1026.0')] ).
cnf(1959,plain,
equal(select(a_1319,i7),e_1246),
inference(rew,[status(thm),theory(equality)],[1944,1032]),
[iquote('9:Rew:1944.0,1032.0')] ).
cnf(1958,plain,
equal(select(a_1315,i7),e_1246),
inference(rew,[status(thm),theory(equality)],[1944,1035]),
[iquote('9:Rew:1944.0,1035.0')] ).
cnf(1957,plain,
equal(select(a_1317,i7),e_1246),
inference(rew,[status(thm),theory(equality)],[1944,1036]),
[iquote('9:Rew:1944.0,1036.0')] ).
cnf(1956,plain,
equal(e_1295,e_1246),
inference(rew,[status(thm),theory(equality)],[1944,757]),
[iquote('9:Rew:1944.0,757.0')] ).
cnf(1955,plain,
equal(e_1299,e_1246),
inference(rew,[status(thm),theory(equality)],[1944,758]),
[iquote('9:Rew:1944.0,758.0')] ).
cnf(1954,plain,
equal(e_1297,e_1246),
inference(rew,[status(thm),theory(equality)],[1944,761]),
[iquote('9:Rew:1944.0,761.0')] ).
cnf(1953,plain,
equal(e_1301,e_1246),
inference(rew,[status(thm),theory(equality)],[1944,766]),
[iquote('9:Rew:1944.0,766.0')] ).
cnf(1952,plain,
equal(e_1303,e_1246),
inference(rew,[status(thm),theory(equality)],[1944,767]),
[iquote('9:Rew:1944.0,767.0')] ).
cnf(1951,plain,
equal(e_1305,e_1246),
inference(rew,[status(thm),theory(equality)],[1944,768]),
[iquote('9:Rew:1944.0,768.0')] ).
cnf(1950,plain,
equal(e_1308,e_1246),
inference(rew,[status(thm),theory(equality)],[1944,774]),
[iquote('9:Rew:1944.0,774.0')] ).
cnf(1949,plain,
equal(e_1310,e_1246),
inference(rew,[status(thm),theory(equality)],[1944,969]),
[iquote('9:Rew:1944.0,969.0')] ).
cnf(1948,plain,
equal(e_1312,e_1246),
inference(rew,[status(thm),theory(equality)],[1944,972]),
[iquote('9:Rew:1944.0,972.0')] ).
cnf(1947,plain,
equal(e_1318,e_1246),
inference(rew,[status(thm),theory(equality)],[1944,1031]),
[iquote('9:Rew:1944.0,1031.0')] ).
cnf(1946,plain,
equal(e_1314,e_1246),
inference(rew,[status(thm),theory(equality)],[1944,1030]),
[iquote('9:Rew:1944.0,1030.0')] ).
cnf(1945,plain,
equal(e_1316,e_1246),
inference(rew,[status(thm),theory(equality)],[1944,1034]),
[iquote('9:Rew:1944.0,1034.0')] ).
cnf(1944,plain,
equal(e_1293,e_1246),
inference(mrr,[status(thm)],[1943,1439]),
[iquote('9:MRR:1943.0,1439.0')] ).
cnf(279,plain,
( equal(i8,u)
| equal(select(a_1292,u),select(a_1290,u)) ),
inference(spr,[status(thm),theory(equality)],[28,2]),
[iquote('0:SpR:28.0,2.1')] ).
cnf(1932,plain,
equal(store(a_1290,i8,e_1244),a_1292),
inference(rew,[status(thm),theory(equality)],[1929,28]),
[iquote('9:Rew:1929.0,28.0')] ).
cnf(1931,plain,
equal(select(a_1292,i8),e_1244),
inference(rew,[status(thm),theory(equality)],[1929,191]),
[iquote('9:Rew:1929.0,191.0')] ).
cnf(1930,plain,
equal(select(a_1288,i7),e_1244),
inference(rew,[status(thm),theory(equality)],[1929,684]),
[iquote('9:Rew:1929.0,684.0')] ).
cnf(1929,plain,
equal(e_1291,e_1244),
inference(mrr,[status(thm)],[1928,1439]),
[iquote('9:MRR:1928.0,1439.0')] ).
cnf(280,plain,
( equal(i8,u)
| equal(select(a_1288,u),select(a_1286,u)) ),
inference(spr,[status(thm),theory(equality)],[26,2]),
[iquote('0:SpR:26.0,2.1')] ).
cnf(1910,plain,
equal(store(a_1286,i8,e_1246),a_1288),
inference(rew,[status(thm),theory(equality)],[1905,26]),
[iquote('9:Rew:1905.0,26.0')] ).
cnf(1909,plain,
equal(store(a_1288,i7,e_1246),a_1290),
inference(rew,[status(thm),theory(equality)],[1905,691]),
[iquote('9:Rew:1905.0,691.0')] ).
cnf(1911,plain,
equal(select(a_1284,i7),e_1246),
inference(rew,[status(thm),theory(equality)],[1905,1655]),
[iquote('9:Rew:1905.0,1655.0')] ).
cnf(1907,plain,
equal(select(a_1290,i7),e_1246),
inference(rew,[status(thm),theory(equality)],[1905,693]),
[iquote('9:Rew:1905.0,693.0')] ).
cnf(1908,plain,
equal(select(a_1288,i8),e_1246),
inference(rew,[status(thm),theory(equality)],[1905,200]),
[iquote('9:Rew:1905.0,200.0')] ).
cnf(1906,plain,
equal(e_1289,e_1246),
inference(rew,[status(thm),theory(equality)],[1905,199]),
[iquote('9:Rew:1905.0,199.0')] ).
cnf(1905,plain,
equal(e_1287,e_1246),
inference(mrr,[status(thm)],[1904,1439]),
[iquote('9:MRR:1904.0,1439.0')] ).
cnf(281,plain,
( equal(i8,u)
| equal(select(a_1284,u),select(a_1283,u)) ),
inference(spr,[status(thm),theory(equality)],[24,2]),
[iquote('0:SpR:24.0,2.1')] ).
cnf(1055,plain,
( equal(i7,u)
| equal(select(a_1319,u),select(a_1292,u)) ),
inference(rew,[status(thm),theory(equality)],[1052,821]),
[iquote('7:Rew:1052.1,821.1')] ).
cnf(1054,plain,
( equal(i7,u)
| equal(select(a_1315,u),select(a_1292,u)) ),
inference(rew,[status(thm),theory(equality)],[1052,738]),
[iquote('7:Rew:1052.1,738.1')] ).
cnf(1053,plain,
( equal(i7,u)
| equal(select(a_1317,u),select(a_1292,u)) ),
inference(rew,[status(thm),theory(equality)],[1052,737]),
[iquote('7:Rew:1052.1,737.1')] ).
cnf(1051,plain,
( equal(i7,u)
| equal(select(a_1282,u),select(a_1253,u)) ),
inference(rew,[status(thm),theory(equality)],[1048,823]),
[iquote('7:Rew:1048.1,823.1')] ).
cnf(1050,plain,
( equal(i7,u)
| equal(select(a_1280,u),select(a_1253,u)) ),
inference(rew,[status(thm),theory(equality)],[1048,822]),
[iquote('7:Rew:1048.1,822.1')] ).
cnf(1049,plain,
( equal(i7,u)
| equal(select(a_1278,u),select(a_1253,u)) ),
inference(rew,[status(thm),theory(equality)],[1048,739]),
[iquote('7:Rew:1048.1,739.1')] ).
cnf(1052,plain,
( equal(i7,u)
| equal(select(a_1313,u),select(a_1292,u)) ),
inference(rew,[status(thm),theory(equality)],[985,1025]),
[iquote('7:Rew:985.1,1025.1')] ).
cnf(1048,plain,
( equal(i7,u)
| equal(select(a_1276,u),select(a_1253,u)) ),
inference(rew,[status(thm),theory(equality)],[983,1024]),
[iquote('7:Rew:983.1,1024.1')] ).
cnf(985,plain,
( equal(i7,u)
| equal(select(a_1311,u),select(a_1292,u)) ),
inference(rew,[status(thm),theory(equality)],[984,398]),
[iquote('6:Rew:984.1,398.1')] ).
cnf(984,plain,
( equal(i7,u)
| equal(select(a_1309,u),select(a_1292,u)) ),
inference(rew,[status(thm),theory(equality)],[810,967]),
[iquote('6:Rew:810.1,967.1')] ).
cnf(983,plain,
( equal(i7,u)
| equal(select(a_1274,u),select(a_1253,u)) ),
inference(rew,[status(thm),theory(equality)],[824,966]),
[iquote('6:Rew:824.1,966.1')] ).
cnf(820,plain,
( equal(i7,u)
| equal(select(a_1265,u),select(a_1253,u)) ),
inference(rew,[status(thm),theory(equality)],[736,813]),
[iquote('5:Rew:736.1,813.1')] ).
cnf(819,plain,
( equal(i7,u)
| equal(select(a_1267,u),select(a_1253,u)) ),
inference(rew,[status(thm),theory(equality)],[736,804]),
[iquote('5:Rew:736.1,804.1')] ).
cnf(818,plain,
( equal(i7,u)
| equal(select(a_1270,u),select(a_1253,u)) ),
inference(rew,[status(thm),theory(equality)],[736,802]),
[iquote('5:Rew:736.1,802.1')] ).
cnf(817,plain,
( equal(i7,u)
| equal(select(a_1269,u),select(a_1253,u)) ),
inference(rew,[status(thm),theory(equality)],[736,801]),
[iquote('5:Rew:736.1,801.1')] ).
cnf(816,plain,
( equal(i7,u)
| equal(select(a_1263,u),select(a_1253,u)) ),
inference(rew,[status(thm),theory(equality)],[736,414]),
[iquote('5:Rew:736.1,414.1')] ).
cnf(815,plain,
( equal(i7,u)
| equal(select(a_1261,u),select(a_1253,u)) ),
inference(rew,[status(thm),theory(equality)],[736,413]),
[iquote('5:Rew:736.1,413.1')] ).
cnf(814,plain,
( equal(i7,u)
| equal(select(a_1259,u),select(a_1253,u)) ),
inference(rew,[status(thm),theory(equality)],[736,402]),
[iquote('5:Rew:736.1,402.1')] ).
cnf(812,plain,
( equal(i7,u)
| equal(select(a_1302,u),select(a_1292,u)) ),
inference(rew,[status(thm),theory(equality)],[734,805]),
[iquote('5:Rew:734.1,805.1')] ).
cnf(811,plain,
( equal(i7,u)
| equal(select(a_1304,u),select(a_1292,u)) ),
inference(rew,[status(thm),theory(equality)],[734,800]),
[iquote('5:Rew:734.1,800.1')] ).
cnf(810,plain,
( equal(i7,u)
| equal(select(a_1307,u),select(a_1292,u)) ),
inference(rew,[status(thm),theory(equality)],[734,799]),
[iquote('5:Rew:734.1,799.1')] ).
cnf(809,plain,
( equal(i7,u)
| equal(select(a_1306,u),select(a_1292,u)) ),
inference(rew,[status(thm),theory(equality)],[734,798]),
[iquote('5:Rew:734.1,798.1')] ).
cnf(808,plain,
( equal(i7,u)
| equal(select(a_1300,u),select(a_1292,u)) ),
inference(rew,[status(thm),theory(equality)],[734,411]),
[iquote('5:Rew:734.1,411.1')] ).
cnf(807,plain,
( equal(i7,u)
| equal(select(a_1298,u),select(a_1292,u)) ),
inference(rew,[status(thm),theory(equality)],[734,399]),
[iquote('5:Rew:734.1,399.1')] ).
cnf(806,plain,
( equal(i7,u)
| equal(select(a_1296,u),select(a_1292,u)) ),
inference(rew,[status(thm),theory(equality)],[734,385]),
[iquote('5:Rew:734.1,385.1')] ).
cnf(824,plain,
( equal(i7,u)
| equal(select(a_1272,u),select(a_1253,u)) ),
inference(rew,[status(thm),theory(equality)],[736,803]),
[iquote('5:Rew:736.1,803.1')] ).
cnf(736,plain,
( equal(i7,u)
| equal(select(a_1257,u),select(a_1253,u)) ),
inference(rew,[status(thm),theory(equality)],[682,605]),
[iquote('5:Rew:682.0,605.0')] ).
cnf(734,plain,
( equal(i7,u)
| equal(select(a_1294,u),select(a_1292,u)) ),
inference(rew,[status(thm),theory(equality)],[682,578]),
[iquote('5:Rew:682.0,578.0')] ).
cnf(696,plain,
( equal(i7,u)
| equal(select(a_1290,u),select(a_1288,u)) ),
inference(rew,[status(thm),theory(equality)],[682,255]),
[iquote('5:Rew:682.0,255.0')] ).
cnf(695,plain,
( equal(i7,u)
| equal(select(a_1255,u),select(a_1253,u)) ),
inference(rew,[status(thm),theory(equality)],[682,256]),
[iquote('5:Rew:682.0,256.0')] ).
cnf(277,plain,
( equal(i7,u)
| equal(select(a_1247,u),select(a_1245,u)) ),
inference(spr,[status(thm),theory(equality)],[4,2]),
[iquote('0:SpR:4.0,2.1')] ).
cnf(276,plain,
( equal(i7,u)
| equal(select(a_1283,u),select(a1,u)) ),
inference(spr,[status(thm),theory(equality)],[23,2]),
[iquote('0:SpR:23.0,2.1')] ).
cnf(289,plain,
( equal(i8,u)
| equal(select(a_1253,u),select(a_1249,u)) ),
inference(rew,[status(thm),theory(equality)],[284,283]),
[iquote('0:Rew:284.1,283.1')] ).
cnf(1825,plain,
equal(store(a_1251,i8,e_1244),a_1253),
inference(rew,[status(thm),theory(equality)],[1822,7]),
[iquote('9:Rew:1822.0,7.0')] ).
cnf(1824,plain,
equal(select(a_1253,i8),e_1244),
inference(rew,[status(thm),theory(equality)],[1822,195]),
[iquote('9:Rew:1822.0,195.0')] ).
cnf(1822,plain,
equal(e_1252,e_1244),
inference(mrr,[status(thm)],[1821,1439]),
[iquote('9:MRR:1821.0,1439.0')] ).
cnf(1823,plain,
equal(select(a_1251,i7),e_1244),
inference(rew,[status(thm),theory(equality)],[1822,686]),
[iquote('9:Rew:1822.0,686.0')] ).
cnf(284,plain,
( equal(i8,u)
| equal(select(a_1251,u),select(a_1249,u)) ),
inference(spr,[status(thm),theory(equality)],[6,2]),
[iquote('0:SpR:6.0,2.1')] ).
cnf(1816,plain,
equal(select(a_1245,i7),e_1244),
inference(mrr,[status(thm)],[1814,1439]),
[iquote('8:MRR:1814.0,1439.0')] ).
cnf(282,plain,
( equal(i8,u)
| equal(select(a1,u),select(a_1245,u)) ),
inference(spr,[status(thm),theory(equality)],[3,2]),
[iquote('0:SpR:3.0,2.1')] ).
cnf(1707,plain,
equal(store(a_1259,i7,e_1246),a_1261),
inference(rew,[status(thm),theory(equality)],[1661,599]),
[iquote('9:Rew:1661.0,599.0')] ).
cnf(1706,plain,
equal(store(a_1257,i7,e_1246),a_1259),
inference(rew,[status(thm),theory(equality)],[1661,603]),
[iquote('9:Rew:1661.0,603.0')] ).
cnf(1705,plain,
equal(store(a_1261,i7,e_1246),a_1263),
inference(rew,[status(thm),theory(equality)],[1661,604]),
[iquote('9:Rew:1661.0,604.0')] ).
cnf(1704,plain,
equal(store(a_1253,i7,e_1246),a_1255),
inference(rew,[status(thm),theory(equality)],[1661,692]),
[iquote('9:Rew:1661.0,692.0')] ).
cnf(1703,plain,
equal(store(a_1263,i7,e_1246),a_1265),
inference(rew,[status(thm),theory(equality)],[1661,789]),
[iquote('9:Rew:1661.0,789.0')] ).
cnf(1702,plain,
equal(store(a_1255,i7,e_1246),a_1257),
inference(rew,[status(thm),theory(equality)],[1661,790]),
[iquote('9:Rew:1661.0,790.0')] ).
cnf(1701,plain,
equal(store(a_1265,i7,e_1246),a_1267),
inference(rew,[status(thm),theory(equality)],[1661,794]),
[iquote('9:Rew:1661.0,794.0')] ).
cnf(1700,plain,
equal(store(a_1269,i7,e_1246),a_1270),
inference(rew,[status(thm),theory(equality)],[1661,795]),
[iquote('9:Rew:1661.0,795.0')] ).
cnf(1699,plain,
equal(store(a_1267,i7,e_1246),a_1269),
inference(rew,[status(thm),theory(equality)],[1661,796]),
[iquote('9:Rew:1661.0,796.0')] ).
cnf(1698,plain,
equal(store(a_1272,i7,e_1246),a_1274),
inference(rew,[status(thm),theory(equality)],[1661,965]),
[iquote('9:Rew:1661.0,965.0')] ).
cnf(1697,plain,
equal(store(a_1270,i7,e_1246),a_1272),
inference(rew,[status(thm),theory(equality)],[1661,977]),
[iquote('9:Rew:1661.0,977.0')] ).
cnf(1696,plain,
equal(store(a_1274,i7,e_1246),a_1276),
inference(rew,[status(thm),theory(equality)],[1661,1029]),
[iquote('9:Rew:1661.0,1029.0')] ).
cnf(1695,plain,
equal(store(a_1278,i7,e_1246),a_1280),
inference(rew,[status(thm),theory(equality)],[1661,1042]),
[iquote('9:Rew:1661.0,1042.0')] ).
cnf(1694,plain,
equal(store(a_1280,i7,e_1246),a_1282),
inference(rew,[status(thm),theory(equality)],[1661,1046]),
[iquote('9:Rew:1661.0,1046.0')] ).
cnf(1693,plain,
equal(store(a_1276,i7,e_1246),a_1278),
inference(rew,[status(thm),theory(equality)],[1661,1047]),
[iquote('9:Rew:1661.0,1047.0')] ).
cnf(1662,plain,
equal(store(a_1249,i8,e_1246),a_1251),
inference(rew,[status(thm),theory(equality)],[1661,6]),
[iquote('9:Rew:1661.0,6.0')] ).
cnf(1658,plain,
equal(store(a_1284,i7,e_1244),a_1286),
inference(rew,[status(thm),theory(equality)],[1652,205]),
[iquote('9:Rew:1652.0,205.0')] ).
cnf(1657,plain,
equal(store(a_1247,i7,e_1244),a_1249),
inference(rew,[status(thm),theory(equality)],[1652,1443]),
[iquote('9:Rew:1652.0,1443.0')] ).
cnf(1692,plain,
equal(select(a_1261,i7),e_1246),
inference(rew,[status(thm),theory(equality)],[1661,598]),
[iquote('9:Rew:1661.0,598.0')] ).
cnf(1691,plain,
equal(select(a_1263,i7),e_1246),
inference(rew,[status(thm),theory(equality)],[1661,601]),
[iquote('9:Rew:1661.0,601.0')] ).
cnf(1689,plain,
equal(select(a_1265,i7),e_1246),
inference(rew,[status(thm),theory(equality)],[1661,770]),
[iquote('9:Rew:1661.0,770.0')] ).
cnf(1690,plain,
equal(select(a_1259,i7),e_1246),
inference(rew,[status(thm),theory(equality)],[1661,602]),
[iquote('9:Rew:1661.0,602.0')] ).
cnf(1688,plain,
equal(select(a_1257,i7),e_1246),
inference(rew,[status(thm),theory(equality)],[1661,771]),
[iquote('9:Rew:1661.0,771.0')] ).
cnf(1687,plain,
equal(select(a_1255,i7),e_1246),
inference(rew,[status(thm),theory(equality)],[1661,747]),
[iquote('9:Rew:1661.0,747.0')] ).
cnf(1686,plain,
equal(select(a_1267,i7),e_1246),
inference(rew,[status(thm),theory(equality)],[1661,779]),
[iquote('9:Rew:1661.0,779.0')] ).
cnf(1685,plain,
equal(select(a_1269,i7),e_1246),
inference(rew,[status(thm),theory(equality)],[1661,785]),
[iquote('9:Rew:1661.0,785.0')] ).
cnf(1684,plain,
equal(select(a_1270,i7),e_1246),
inference(rew,[status(thm),theory(equality)],[1661,784]),
[iquote('9:Rew:1661.0,784.0')] ).
cnf(1683,plain,
equal(select(a_1274,i7),e_1246),
inference(rew,[status(thm),theory(equality)],[1661,981]),
[iquote('9:Rew:1661.0,981.0')] ).
cnf(1682,plain,
equal(select(a_1272,i7),e_1246),
inference(rew,[status(thm),theory(equality)],[1661,976]),
[iquote('9:Rew:1661.0,976.0')] ).
cnf(1681,plain,
equal(select(a_1276,i7),e_1246),
inference(rew,[status(thm),theory(equality)],[1661,1027]),
[iquote('9:Rew:1661.0,1027.0')] ).
cnf(1679,plain,
equal(select(a_1280,i7),e_1246),
inference(rew,[status(thm),theory(equality)],[1661,1041]),
[iquote('9:Rew:1661.0,1041.0')] ).
cnf(1680,plain,
equal(select(a_1278,i7),e_1246),
inference(rew,[status(thm),theory(equality)],[1661,1044]),
[iquote('9:Rew:1661.0,1044.0')] ).
cnf(1678,plain,
equal(select(a_1282,i7),e_1246),
inference(rew,[status(thm),theory(equality)],[1661,1045]),
[iquote('9:Rew:1661.0,1045.0')] ).
cnf(1664,plain,
equal(select(a_1251,i8),e_1246),
inference(rew,[status(thm),theory(equality)],[1661,207]),
[iquote('9:Rew:1661.0,207.0')] ).
cnf(1656,plain,
equal(select(a_1286,i7),e_1244),
inference(rew,[status(thm),theory(equality)],[1652,210]),
[iquote('9:Rew:1652.0,210.0')] ).
cnf(1654,plain,
equal(select(a_1249,i7),e_1244),
inference(rew,[status(thm),theory(equality)],[1652,1441]),
[iquote('9:Rew:1652.0,1441.0')] ).
cnf(1677,plain,
equal(e_1281,e_1246),
inference(rew,[status(thm),theory(equality)],[1661,1043]),
[iquote('9:Rew:1661.0,1043.0')] ).
cnf(1676,plain,
equal(e_1279,e_1246),
inference(rew,[status(thm),theory(equality)],[1661,1040]),
[iquote('9:Rew:1661.0,1040.0')] ).
cnf(1675,plain,
equal(e_1277,e_1246),
inference(rew,[status(thm),theory(equality)],[1661,1039]),
[iquote('9:Rew:1661.0,1039.0')] ).
cnf(1674,plain,
equal(e_1275,e_1246),
inference(rew,[status(thm),theory(equality)],[1661,978]),
[iquote('9:Rew:1661.0,978.0')] ).
cnf(1673,plain,
equal(e_1271,e_1246),
inference(rew,[status(thm),theory(equality)],[1661,975]),
[iquote('9:Rew:1661.0,975.0')] ).
cnf(1672,plain,
equal(e_1273,e_1246),
inference(rew,[status(thm),theory(equality)],[1661,781]),
[iquote('9:Rew:1661.0,781.0')] ).
cnf(1671,plain,
equal(e_1256,e_1246),
inference(rew,[status(thm),theory(equality)],[1661,746]),
[iquote('9:Rew:1661.0,746.0')] ).
cnf(1670,plain,
equal(e_1268,e_1246),
inference(rew,[status(thm),theory(equality)],[1661,745]),
[iquote('9:Rew:1661.0,745.0')] ).
cnf(1669,plain,
equal(e_1266,e_1246),
inference(rew,[status(thm),theory(equality)],[1661,744]),
[iquote('9:Rew:1661.0,744.0')] ).
cnf(1668,plain,
equal(e_1264,e_1246),
inference(rew,[status(thm),theory(equality)],[1661,743]),
[iquote('9:Rew:1661.0,743.0')] ).
cnf(1667,plain,
equal(e_1262,e_1246),
inference(rew,[status(thm),theory(equality)],[1661,600]),
[iquote('9:Rew:1661.0,600.0')] ).
cnf(1666,plain,
equal(e_1260,e_1246),
inference(rew,[status(thm),theory(equality)],[1661,597]),
[iquote('9:Rew:1661.0,597.0')] ).
cnf(1665,plain,
equal(e_1258,e_1246),
inference(rew,[status(thm),theory(equality)],[1661,596]),
[iquote('9:Rew:1661.0,596.0')] ).
cnf(1663,plain,
equal(e_1254,e_1246),
inference(rew,[status(thm),theory(equality)],[1661,206]),
[iquote('9:Rew:1661.0,206.0')] ).
cnf(1661,plain,
equal(e_1250,e_1246),
inference(rew,[status(thm),theory(equality)],[189,1653]),
[iquote('9:Rew:189.0,1653.0')] ).
cnf(1652,plain,
equal(i6,i7),
inference(spt,[],[1105]),
[iquote('9:Spt:1105.0')] ).
cnf(24,axiom,
equal(store(a_1283,i8,e_1244),a_1284),
file('SWV533-1.010.p',unknown),
[] ).
cnf(23,axiom,
equal(store(a1,i7,e_1246),a_1283),
file('SWV533-1.010.p',unknown),
[] ).
cnf(4,axiom,
equal(store(a_1245,i7,e_1246),a_1247),
file('SWV533-1.010.p',unknown),
[] ).
cnf(204,plain,
equal(select(a_1284,i8),e_1244),
inference(rew,[status(thm),theory(equality)],[203,62]),
[iquote('0:Rew:203.0,62.0')] ).
cnf(1442,plain,
equal(select(a_1247,i8),e_1244),
inference(rew,[status(thm),theory(equality)],[1440,45]),
[iquote('8:Rew:1440.0,45.0')] ).
cnf(44,axiom,
equal(select(a1,i8),e_1246),
file('SWV533-1.010.p',unknown),
[] ).
cnf(188,plain,
equal(select(a_1283,i7),e_1246),
inference(spr,[status(thm),theory(equality)],[23,1]),
[iquote('0:SpR:23.0,1.0')] ).
cnf(43,axiom,
equal(select(a1,i7),e_1244),
file('SWV533-1.010.p',unknown),
[] ).
cnf(189,plain,
equal(select(a_1247,i7),e_1246),
inference(spr,[status(thm),theory(equality)],[4,1]),
[iquote('0:SpR:4.0,1.0')] ).
cnf(1439,plain,
~ equal(i7,i8),
inference(spt,[],[1400,1109,1110]),
[iquote('8:Spt:1400.0,1109.0,1110.0')] ).
cnf(371,plain,
equal(i9,i7),
inference(spt,[],[312]),
[iquote('2:Spt:312.0')] ).
cnf(387,plain,
equal(i1,i7),
inference(rew,[status(thm),theory(equality)],[371,317]),
[iquote('2:Rew:371.0,317.0')] ).
cnf(682,plain,
equal(i5,i7),
inference(spt,[],[561]),
[iquote('5:Spt:561.0')] ).
cnf(698,plain,
equal(i0,i7),
inference(rew,[status(thm),theory(equality)],[682,464]),
[iquote('5:Rew:682.0,464.0')] ).
cnf(705,plain,
equal(i4,i7),
inference(rew,[status(thm),theory(equality)],[682,563]),
[iquote('5:Rew:682.0,563.0')] ).
cnf(959,plain,
equal(i2,i7),
inference(spt,[],[958]),
[iquote('6:Spt:958.0')] ).
cnf(1021,plain,
equal(i3,i7),
inference(spt,[],[982]),
[iquote('7:Spt:982.0')] ).
cnf(1440,plain,
equal(e_1248,e_1244),
inference(spt,[],[1400,1109]),
[iquote('8:Spt:1400.0,1109.1')] ).
cnf(80,plain,
equal(select(store(u,a_1319,v),a_1282),select(u,a_1282)),
inference(res,[status(thm),theory(equality)],[2,79]),
[iquote('0:Res:2.0,79.0')] ).
cnf(81,plain,
equal(select(store(u,a_1282,v),a_1319),select(u,a_1319)),
inference(res,[status(thm),theory(equality)],[2,79]),
[iquote('0:Res:2.0,79.0')] ).
cnf(194,plain,
equal(select(a_1245,i8),e_1244),
inference(spr,[status(thm),theory(equality)],[3,1]),
[iquote('0:SpR:3.0,1.0')] ).
cnf(2,axiom,
( equal(u,v)
| equal(select(store(w,u,x),v),select(w,v)) ),
file('SWV533-1.010.p',unknown),
[] ).
cnf(203,plain,
equal(e_1285,e_1244),
inference(rew,[status(thm),theory(equality)],[62,193]),
[iquote('0:Rew:62.0,193.0')] ).
cnf(1,axiom,
equal(select(store(u,v,w),v),w),
file('SWV533-1.010.p',unknown),
[] ).
cnf(3,axiom,
equal(store(a1,i8,e_1244),a_1245),
file('SWV533-1.010.p',unknown),
[] ).
cnf(79,axiom,
~ equal(a_1319,a_1282),
file('SWV533-1.010.p',unknown),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : SWV533-1.010 : TPTP v8.1.0. Released v4.0.0.
% 0.10/0.13 % Command : run_spass %d %s
% 0.13/0.34 % Computer : n029.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Wed Jun 15 12:03:26 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.44/0.60
% 0.44/0.60 SPASS V 3.9
% 0.44/0.60 SPASS beiseite: Completion found.
% 0.44/0.60 % SZS status CounterSatisfiable
% 0.44/0.60 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.44/0.60 SPASS derived 1713 clauses, backtracked 142 clauses, performed 9 splits and kept 921 clauses.
% 0.44/0.60 SPASS allocated 64166 KBytes.
% 0.44/0.60 SPASS spent 0:00:00.25 on the problem.
% 0.44/0.60 0:00:00.04 for the input.
% 0.44/0.60 0:00:00.00 for the FLOTTER CNF translation.
% 0.44/0.60 0:00:00.02 for inferences.
% 0.44/0.60 0:00:00.00 for the backtracking.
% 0.44/0.60 0:00:00.15 for the reduction.
% 0.44/0.60
% 0.44/0.60
% 0.44/0.60 The saturated set of worked-off clauses is :
% 0.44/0.60 % SZS output start Saturation
% See solution above
%------------------------------------------------------------------------------