%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SWV507-1.030 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n004.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:43:43 EDT 2022
% Result : Satisfiable 0.21s 0.50s
% Output : Saturation 0.21s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 327)
% Comments :
%------------------------------------------------------------------------------
cnf(444,plain,
equal(select(store(u,e10,v),e30),select(u,e30)),
inference(rew,[status(thm),theory(equality)],[440,331]),
[iquote('2:Rew:440.0,331.0')] ).
cnf(443,plain,
equal(select(store(u,e30,v),e10),select(u,e10)),
inference(rew,[status(thm),theory(equality)],[440,330]),
[iquote('2:Rew:440.0,330.0')] ).
cnf(439,plain,
( equal(n10,u)
| equal(select(a_1104,u),select(a_1103,u)) ),
inference(rew,[status(thm),theory(equality)],[433,247]),
[iquote('2:Rew:433.0,247.0')] ).
cnf(438,plain,
( equal(n10,u)
| equal(select(a_1098,u),select(a_1097,u)) ),
inference(rew,[status(thm),theory(equality)],[433,248]),
[iquote('2:Rew:433.0,248.0')] ).
cnf(258,plain,
( equal(n13,u)
| equal(select(a_1081,u),select(a_1080,u)) ),
inference(spr,[status(thm),theory(equality)],[15,2]),
[iquote('0:SpR:15.0,2.1')] ).
cnf(257,plain,
( equal(n13,u)
| equal(select(a_1099,u),select(a1,u)) ),
inference(spr,[status(thm),theory(equality)],[33,2]),
[iquote('0:SpR:33.0,2.1')] ).
cnf(256,plain,
( equal(n1,u)
| equal(select(a1,u),select(a_1069,u)) ),
inference(spr,[status(thm),theory(equality)],[3,2]),
[iquote('0:SpR:3.0,2.1')] ).
cnf(255,plain,
( equal(n1,u)
| equal(select(a_1100,u),select(a_1099,u)) ),
inference(spr,[status(thm),theory(equality)],[34,2]),
[iquote('0:SpR:34.0,2.1')] ).
cnf(254,plain,
( equal(n19,u)
| equal(select(a_1087,u),select(a_1086,u)) ),
inference(spr,[status(thm),theory(equality)],[21,2]),
[iquote('0:SpR:21.0,2.1')] ).
cnf(253,plain,
( equal(n19,u)
| equal(select(a_1101,u),select(a_1100,u)) ),
inference(spr,[status(thm),theory(equality)],[35,2]),
[iquote('0:SpR:35.0,2.1')] ).
cnf(252,plain,
( equal(n4,u)
| equal(select(a_1072,u),select(a_1071,u)) ),
inference(spr,[status(thm),theory(equality)],[6,2]),
[iquote('0:SpR:6.0,2.1')] ).
cnf(251,plain,
( equal(n4,u)
| equal(select(a_1102,u),select(a_1101,u)) ),
inference(spr,[status(thm),theory(equality)],[36,2]),
[iquote('0:SpR:36.0,2.1')] ).
cnf(250,plain,
( equal(n9,u)
| equal(select(a_1077,u),select(a_1076,u)) ),
inference(spr,[status(thm),theory(equality)],[11,2]),
[iquote('0:SpR:11.0,2.1')] ).
cnf(249,plain,
( equal(n9,u)
| equal(select(a_1103,u),select(a_1102,u)) ),
inference(spr,[status(thm),theory(equality)],[37,2]),
[iquote('0:SpR:37.0,2.1')] ).
cnf(435,plain,
equal(store(a_1097,n10,e30),a_1098),
inference(rew,[status(thm),theory(equality)],[433,32]),
[iquote('2:Rew:433.0,32.0')] ).
cnf(434,plain,
equal(store(a_1103,n10,e30),a_1104),
inference(rew,[status(thm),theory(equality)],[433,38]),
[iquote('2:Rew:433.0,38.0')] ).
cnf(442,plain,
equal(select(a_1098,n10),e30),
inference(rew,[status(thm),theory(equality)],[440,327]),
[iquote('2:Rew:440.0,327.0')] ).
cnf(436,plain,
equal(select(a_1104,n10),e30),
inference(rew,[status(thm),theory(equality)],[433,181]),
[iquote('2:Rew:433.0,181.0')] ).
cnf(440,plain,
equal(e_1130,e30),
inference(rew,[status(thm),theory(equality)],[327,437]),
[iquote('2:Rew:327.0,437.0')] ).
cnf(441,plain,
~ equal(e30,e10),
inference(rew,[status(thm),theory(equality)],[440,329]),
[iquote('2:Rew:440.0,329.0')] ).
cnf(433,plain,
equal(n30,n10),
inference(spt,[],[430]),
[iquote('2:Spt:430.0')] ).
cnf(246,plain,
( equal(n2,u)
| equal(select(a_1070,u),select(a_1069,u)) ),
inference(spr,[status(thm),theory(equality)],[4,2]),
[iquote('0:SpR:4.0,2.1')] ).
cnf(245,plain,
( equal(n2,u)
| equal(select(a_1105,u),select(a_1104,u)) ),
inference(spr,[status(thm),theory(equality)],[39,2]),
[iquote('0:SpR:39.0,2.1')] ).
cnf(244,plain,
( equal(n15,u)
| equal(select(a_1083,u),select(a_1082,u)) ),
inference(spr,[status(thm),theory(equality)],[17,2]),
[iquote('0:SpR:17.0,2.1')] ).
cnf(243,plain,
( equal(n15,u)
| equal(select(a_1106,u),select(a_1105,u)) ),
inference(spr,[status(thm),theory(equality)],[40,2]),
[iquote('0:SpR:40.0,2.1')] ).
cnf(242,plain,
( equal(n25,u)
| equal(select(a_1093,u),select(a_1092,u)) ),
inference(spr,[status(thm),theory(equality)],[27,2]),
[iquote('0:SpR:27.0,2.1')] ).
cnf(241,plain,
( equal(n25,u)
| equal(select(a_1107,u),select(a_1106,u)) ),
inference(spr,[status(thm),theory(equality)],[41,2]),
[iquote('0:SpR:41.0,2.1')] ).
cnf(240,plain,
( equal(n18,u)
| equal(select(a_1086,u),select(a_1085,u)) ),
inference(spr,[status(thm),theory(equality)],[20,2]),
[iquote('0:SpR:20.0,2.1')] ).
cnf(239,plain,
( equal(n18,u)
| equal(select(a_1108,u),select(a_1107,u)) ),
inference(spr,[status(thm),theory(equality)],[42,2]),
[iquote('0:SpR:42.0,2.1')] ).
cnf(238,plain,
( equal(n20,u)
| equal(select(a_1088,u),select(a_1087,u)) ),
inference(spr,[status(thm),theory(equality)],[22,2]),
[iquote('0:SpR:22.0,2.1')] ).
cnf(237,plain,
( equal(n20,u)
| equal(select(a_1109,u),select(a_1108,u)) ),
inference(spr,[status(thm),theory(equality)],[43,2]),
[iquote('0:SpR:43.0,2.1')] ).
cnf(236,plain,
( equal(n8,u)
| equal(select(a_1076,u),select(a_1075,u)) ),
inference(spr,[status(thm),theory(equality)],[10,2]),
[iquote('0:SpR:10.0,2.1')] ).
cnf(235,plain,
( equal(n8,u)
| equal(select(a_1110,u),select(a_1109,u)) ),
inference(spr,[status(thm),theory(equality)],[44,2]),
[iquote('0:SpR:44.0,2.1')] ).
cnf(234,plain,
( equal(n21,u)
| equal(select(a_1089,u),select(a_1088,u)) ),
inference(spr,[status(thm),theory(equality)],[23,2]),
[iquote('0:SpR:23.0,2.1')] ).
cnf(233,plain,
( equal(n21,u)
| equal(select(a_1111,u),select(a_1110,u)) ),
inference(spr,[status(thm),theory(equality)],[45,2]),
[iquote('0:SpR:45.0,2.1')] ).
cnf(232,plain,
( equal(n6,u)
| equal(select(a_1074,u),select(a_1073,u)) ),
inference(spr,[status(thm),theory(equality)],[8,2]),
[iquote('0:SpR:8.0,2.1')] ).
cnf(231,plain,
( equal(n6,u)
| equal(select(a_1112,u),select(a_1111,u)) ),
inference(spr,[status(thm),theory(equality)],[46,2]),
[iquote('0:SpR:46.0,2.1')] ).
cnf(230,plain,
( equal(n11,u)
| equal(select(a_1079,u),select(a_1078,u)) ),
inference(spr,[status(thm),theory(equality)],[13,2]),
[iquote('0:SpR:13.0,2.1')] ).
cnf(229,plain,
( equal(n11,u)
| equal(select(a_1113,u),select(a_1112,u)) ),
inference(spr,[status(thm),theory(equality)],[47,2]),
[iquote('0:SpR:47.0,2.1')] ).
cnf(228,plain,
( equal(n14,u)
| equal(select(a_1082,u),select(a_1081,u)) ),
inference(spr,[status(thm),theory(equality)],[16,2]),
[iquote('0:SpR:16.0,2.1')] ).
cnf(227,plain,
( equal(n14,u)
| equal(select(a_1114,u),select(a_1113,u)) ),
inference(spr,[status(thm),theory(equality)],[48,2]),
[iquote('0:SpR:48.0,2.1')] ).
cnf(226,plain,
( equal(n29,u)
| equal(select(a_1097,u),select(a_1096,u)) ),
inference(spr,[status(thm),theory(equality)],[31,2]),
[iquote('0:SpR:31.0,2.1')] ).
cnf(225,plain,
( equal(n29,u)
| equal(select(a_1115,u),select(a_1114,u)) ),
inference(spr,[status(thm),theory(equality)],[49,2]),
[iquote('0:SpR:49.0,2.1')] ).
cnf(224,plain,
( equal(n5,u)
| equal(select(a_1073,u),select(a_1072,u)) ),
inference(spr,[status(thm),theory(equality)],[7,2]),
[iquote('0:SpR:7.0,2.1')] ).
cnf(223,plain,
( equal(n5,u)
| equal(select(a_1116,u),select(a_1115,u)) ),
inference(spr,[status(thm),theory(equality)],[50,2]),
[iquote('0:SpR:50.0,2.1')] ).
cnf(222,plain,
( equal(n26,u)
| equal(select(a_1094,u),select(a_1093,u)) ),
inference(spr,[status(thm),theory(equality)],[28,2]),
[iquote('0:SpR:28.0,2.1')] ).
cnf(221,plain,
( equal(n26,u)
| equal(select(a_1117,u),select(a_1116,u)) ),
inference(spr,[status(thm),theory(equality)],[51,2]),
[iquote('0:SpR:51.0,2.1')] ).
cnf(220,plain,
( equal(n22,u)
| equal(select(a_1090,u),select(a_1089,u)) ),
inference(spr,[status(thm),theory(equality)],[24,2]),
[iquote('0:SpR:24.0,2.1')] ).
cnf(219,plain,
( equal(n22,u)
| equal(select(a_1118,u),select(a_1117,u)) ),
inference(spr,[status(thm),theory(equality)],[52,2]),
[iquote('0:SpR:52.0,2.1')] ).
cnf(218,plain,
( equal(n27,u)
| equal(select(a_1095,u),select(a_1094,u)) ),
inference(spr,[status(thm),theory(equality)],[29,2]),
[iquote('0:SpR:29.0,2.1')] ).
cnf(217,plain,
( equal(n27,u)
| equal(select(a_1119,u),select(a_1118,u)) ),
inference(spr,[status(thm),theory(equality)],[53,2]),
[iquote('0:SpR:53.0,2.1')] ).
cnf(216,plain,
( equal(n3,u)
| equal(select(a_1071,u),select(a_1070,u)) ),
inference(spr,[status(thm),theory(equality)],[5,2]),
[iquote('0:SpR:5.0,2.1')] ).
cnf(215,plain,
( equal(n3,u)
| equal(select(a_1120,u),select(a_1119,u)) ),
inference(spr,[status(thm),theory(equality)],[54,2]),
[iquote('0:SpR:54.0,2.1')] ).
cnf(214,plain,
( equal(n12,u)
| equal(select(a_1080,u),select(a_1079,u)) ),
inference(spr,[status(thm),theory(equality)],[14,2]),
[iquote('0:SpR:14.0,2.1')] ).
cnf(213,plain,
( equal(n12,u)
| equal(select(a_1121,u),select(a_1120,u)) ),
inference(spr,[status(thm),theory(equality)],[55,2]),
[iquote('0:SpR:55.0,2.1')] ).
cnf(212,plain,
( equal(n16,u)
| equal(select(a_1084,u),select(a_1083,u)) ),
inference(spr,[status(thm),theory(equality)],[18,2]),
[iquote('0:SpR:18.0,2.1')] ).
cnf(211,plain,
( equal(n16,u)
| equal(select(a_1122,u),select(a_1121,u)) ),
inference(spr,[status(thm),theory(equality)],[56,2]),
[iquote('0:SpR:56.0,2.1')] ).
cnf(210,plain,
( equal(n28,u)
| equal(select(a_1096,u),select(a_1095,u)) ),
inference(spr,[status(thm),theory(equality)],[30,2]),
[iquote('0:SpR:30.0,2.1')] ).
cnf(209,plain,
( equal(n28,u)
| equal(select(a_1123,u),select(a_1122,u)) ),
inference(spr,[status(thm),theory(equality)],[57,2]),
[iquote('0:SpR:57.0,2.1')] ).
cnf(208,plain,
( equal(n17,u)
| equal(select(a_1085,u),select(a_1084,u)) ),
inference(spr,[status(thm),theory(equality)],[19,2]),
[iquote('0:SpR:19.0,2.1')] ).
cnf(207,plain,
( equal(n17,u)
| equal(select(a_1124,u),select(a_1123,u)) ),
inference(spr,[status(thm),theory(equality)],[58,2]),
[iquote('0:SpR:58.0,2.1')] ).
cnf(206,plain,
( equal(n23,u)
| equal(select(a_1091,u),select(a_1090,u)) ),
inference(spr,[status(thm),theory(equality)],[25,2]),
[iquote('0:SpR:25.0,2.1')] ).
cnf(205,plain,
( equal(n23,u)
| equal(select(a_1125,u),select(a_1124,u)) ),
inference(spr,[status(thm),theory(equality)],[59,2]),
[iquote('0:SpR:59.0,2.1')] ).
cnf(204,plain,
( equal(n24,u)
| equal(select(a_1092,u),select(a_1091,u)) ),
inference(spr,[status(thm),theory(equality)],[26,2]),
[iquote('0:SpR:26.0,2.1')] ).
cnf(203,plain,
( equal(n24,u)
| equal(select(a_1126,u),select(a_1125,u)) ),
inference(spr,[status(thm),theory(equality)],[60,2]),
[iquote('0:SpR:60.0,2.1')] ).
cnf(202,plain,
( equal(n7,u)
| equal(select(a_1075,u),select(a_1074,u)) ),
inference(spr,[status(thm),theory(equality)],[9,2]),
[iquote('0:SpR:9.0,2.1')] ).
cnf(201,plain,
( equal(n7,u)
| equal(select(a_1127,u),select(a_1126,u)) ),
inference(spr,[status(thm),theory(equality)],[61,2]),
[iquote('0:SpR:61.0,2.1')] ).
cnf(325,plain,
equal(sk(a_1098,a_1128),n10),
inference(rew,[status(thm),theory(equality)],[324,65]),
[iquote('1:Rew:324.0,65.0')] ).
cnf(328,plain,
equal(e_1131,e10),
inference(rew,[status(thm),theory(equality)],[133,326]),
[iquote('1:Rew:133.0,326.0')] ).
cnf(324,plain,
equal(i_1129,n10),
inference(spt,[],[319]),
[iquote('1:Spt:319.0')] ).
cnf(200,plain,
( equal(n10,u)
| equal(select(a_1078,u),select(a_1077,u)) ),
inference(spr,[status(thm),theory(equality)],[12,2]),
[iquote('0:SpR:12.0,2.1')] ).
cnf(199,plain,
( equal(n10,u)
| equal(select(a_1128,u),select(a_1127,u)) ),
inference(spr,[status(thm),theory(equality)],[62,2]),
[iquote('0:SpR:62.0,2.1')] ).
cnf(192,plain,
equal(select(a_1081,n13),e13),
inference(spr,[status(thm),theory(equality)],[15,1]),
[iquote('0:SpR:15.0,1.0')] ).
cnf(191,plain,
equal(select(a_1099,n13),e13),
inference(spr,[status(thm),theory(equality)],[33,1]),
[iquote('0:SpR:33.0,1.0')] ).
cnf(190,plain,
equal(select(a_1069,n1),e1),
inference(spr,[status(thm),theory(equality)],[3,1]),
[iquote('0:SpR:3.0,1.0')] ).
cnf(189,plain,
equal(select(a_1100,n1),e1),
inference(spr,[status(thm),theory(equality)],[34,1]),
[iquote('0:SpR:34.0,1.0')] ).
cnf(188,plain,
equal(select(a_1087,n19),e19),
inference(spr,[status(thm),theory(equality)],[21,1]),
[iquote('0:SpR:21.0,1.0')] ).
cnf(187,plain,
equal(select(a_1101,n19),e19),
inference(spr,[status(thm),theory(equality)],[35,1]),
[iquote('0:SpR:35.0,1.0')] ).
cnf(186,plain,
equal(select(a_1072,n4),e4),
inference(spr,[status(thm),theory(equality)],[6,1]),
[iquote('0:SpR:6.0,1.0')] ).
cnf(185,plain,
equal(select(a_1102,n4),e4),
inference(spr,[status(thm),theory(equality)],[36,1]),
[iquote('0:SpR:36.0,1.0')] ).
cnf(184,plain,
equal(select(a_1077,n9),e9),
inference(spr,[status(thm),theory(equality)],[11,1]),
[iquote('0:SpR:11.0,1.0')] ).
cnf(183,plain,
equal(select(a_1103,n9),e9),
inference(spr,[status(thm),theory(equality)],[37,1]),
[iquote('0:SpR:37.0,1.0')] ).
cnf(180,plain,
equal(select(a_1070,n2),e2),
inference(spr,[status(thm),theory(equality)],[4,1]),
[iquote('0:SpR:4.0,1.0')] ).
cnf(179,plain,
equal(select(a_1105,n2),e2),
inference(spr,[status(thm),theory(equality)],[39,1]),
[iquote('0:SpR:39.0,1.0')] ).
cnf(178,plain,
equal(select(a_1083,n15),e15),
inference(spr,[status(thm),theory(equality)],[17,1]),
[iquote('0:SpR:17.0,1.0')] ).
cnf(177,plain,
equal(select(a_1106,n15),e15),
inference(spr,[status(thm),theory(equality)],[40,1]),
[iquote('0:SpR:40.0,1.0')] ).
cnf(176,plain,
equal(select(a_1093,n25),e25),
inference(spr,[status(thm),theory(equality)],[27,1]),
[iquote('0:SpR:27.0,1.0')] ).
cnf(175,plain,
equal(select(a_1107,n25),e25),
inference(spr,[status(thm),theory(equality)],[41,1]),
[iquote('0:SpR:41.0,1.0')] ).
cnf(174,plain,
equal(select(a_1086,n18),e18),
inference(spr,[status(thm),theory(equality)],[20,1]),
[iquote('0:SpR:20.0,1.0')] ).
cnf(173,plain,
equal(select(a_1108,n18),e18),
inference(spr,[status(thm),theory(equality)],[42,1]),
[iquote('0:SpR:42.0,1.0')] ).
cnf(172,plain,
equal(select(a_1088,n20),e20),
inference(spr,[status(thm),theory(equality)],[22,1]),
[iquote('0:SpR:22.0,1.0')] ).
cnf(171,plain,
equal(select(a_1109,n20),e20),
inference(spr,[status(thm),theory(equality)],[43,1]),
[iquote('0:SpR:43.0,1.0')] ).
cnf(170,plain,
equal(select(a_1076,n8),e8),
inference(spr,[status(thm),theory(equality)],[10,1]),
[iquote('0:SpR:10.0,1.0')] ).
cnf(169,plain,
equal(select(a_1110,n8),e8),
inference(spr,[status(thm),theory(equality)],[44,1]),
[iquote('0:SpR:44.0,1.0')] ).
cnf(168,plain,
equal(select(a_1089,n21),e21),
inference(spr,[status(thm),theory(equality)],[23,1]),
[iquote('0:SpR:23.0,1.0')] ).
cnf(167,plain,
equal(select(a_1111,n21),e21),
inference(spr,[status(thm),theory(equality)],[45,1]),
[iquote('0:SpR:45.0,1.0')] ).
cnf(166,plain,
equal(select(a_1074,n6),e6),
inference(spr,[status(thm),theory(equality)],[8,1]),
[iquote('0:SpR:8.0,1.0')] ).
cnf(165,plain,
equal(select(a_1112,n6),e6),
inference(spr,[status(thm),theory(equality)],[46,1]),
[iquote('0:SpR:46.0,1.0')] ).
cnf(164,plain,
equal(select(a_1079,n11),e11),
inference(spr,[status(thm),theory(equality)],[13,1]),
[iquote('0:SpR:13.0,1.0')] ).
cnf(163,plain,
equal(select(a_1113,n11),e11),
inference(spr,[status(thm),theory(equality)],[47,1]),
[iquote('0:SpR:47.0,1.0')] ).
cnf(162,plain,
equal(select(a_1082,n14),e14),
inference(spr,[status(thm),theory(equality)],[16,1]),
[iquote('0:SpR:16.0,1.0')] ).
cnf(161,plain,
equal(select(a_1114,n14),e14),
inference(spr,[status(thm),theory(equality)],[48,1]),
[iquote('0:SpR:48.0,1.0')] ).
cnf(160,plain,
equal(select(a_1097,n29),e29),
inference(spr,[status(thm),theory(equality)],[31,1]),
[iquote('0:SpR:31.0,1.0')] ).
cnf(159,plain,
equal(select(a_1115,n29),e29),
inference(spr,[status(thm),theory(equality)],[49,1]),
[iquote('0:SpR:49.0,1.0')] ).
cnf(158,plain,
equal(select(a_1073,n5),e5),
inference(spr,[status(thm),theory(equality)],[7,1]),
[iquote('0:SpR:7.0,1.0')] ).
cnf(157,plain,
equal(select(a_1116,n5),e5),
inference(spr,[status(thm),theory(equality)],[50,1]),
[iquote('0:SpR:50.0,1.0')] ).
cnf(156,plain,
equal(select(a_1094,n26),e26),
inference(spr,[status(thm),theory(equality)],[28,1]),
[iquote('0:SpR:28.0,1.0')] ).
cnf(155,plain,
equal(select(a_1117,n26),e26),
inference(spr,[status(thm),theory(equality)],[51,1]),
[iquote('0:SpR:51.0,1.0')] ).
cnf(154,plain,
equal(select(a_1090,n22),e22),
inference(spr,[status(thm),theory(equality)],[24,1]),
[iquote('0:SpR:24.0,1.0')] ).
cnf(153,plain,
equal(select(a_1118,n22),e22),
inference(spr,[status(thm),theory(equality)],[52,1]),
[iquote('0:SpR:52.0,1.0')] ).
cnf(152,plain,
equal(select(a_1095,n27),e27),
inference(spr,[status(thm),theory(equality)],[29,1]),
[iquote('0:SpR:29.0,1.0')] ).
cnf(151,plain,
equal(select(a_1119,n27),e27),
inference(spr,[status(thm),theory(equality)],[53,1]),
[iquote('0:SpR:53.0,1.0')] ).
cnf(150,plain,
equal(select(a_1071,n3),e3),
inference(spr,[status(thm),theory(equality)],[5,1]),
[iquote('0:SpR:5.0,1.0')] ).
cnf(149,plain,
equal(select(a_1120,n3),e3),
inference(spr,[status(thm),theory(equality)],[54,1]),
[iquote('0:SpR:54.0,1.0')] ).
cnf(148,plain,
equal(select(a_1080,n12),e12),
inference(spr,[status(thm),theory(equality)],[14,1]),
[iquote('0:SpR:14.0,1.0')] ).
cnf(147,plain,
equal(select(a_1121,n12),e12),
inference(spr,[status(thm),theory(equality)],[55,1]),
[iquote('0:SpR:55.0,1.0')] ).
cnf(146,plain,
equal(select(a_1084,n16),e16),
inference(spr,[status(thm),theory(equality)],[18,1]),
[iquote('0:SpR:18.0,1.0')] ).
cnf(145,plain,
equal(select(a_1122,n16),e16),
inference(spr,[status(thm),theory(equality)],[56,1]),
[iquote('0:SpR:56.0,1.0')] ).
cnf(144,plain,
equal(select(a_1096,n28),e28),
inference(spr,[status(thm),theory(equality)],[30,1]),
[iquote('0:SpR:30.0,1.0')] ).
cnf(143,plain,
equal(select(a_1123,n28),e28),
inference(spr,[status(thm),theory(equality)],[57,1]),
[iquote('0:SpR:57.0,1.0')] ).
cnf(142,plain,
equal(select(a_1085,n17),e17),
inference(spr,[status(thm),theory(equality)],[19,1]),
[iquote('0:SpR:19.0,1.0')] ).
cnf(141,plain,
equal(select(a_1124,n17),e17),
inference(spr,[status(thm),theory(equality)],[58,1]),
[iquote('0:SpR:58.0,1.0')] ).
cnf(140,plain,
equal(select(a_1091,n23),e23),
inference(spr,[status(thm),theory(equality)],[25,1]),
[iquote('0:SpR:25.0,1.0')] ).
cnf(139,plain,
equal(select(a_1125,n23),e23),
inference(spr,[status(thm),theory(equality)],[59,1]),
[iquote('0:SpR:59.0,1.0')] ).
cnf(138,plain,
equal(select(a_1092,n24),e24),
inference(spr,[status(thm),theory(equality)],[26,1]),
[iquote('0:SpR:26.0,1.0')] ).
cnf(137,plain,
equal(select(a_1126,n24),e24),
inference(spr,[status(thm),theory(equality)],[60,1]),
[iquote('0:SpR:60.0,1.0')] ).
cnf(2,axiom,
( equal(u,v)
| equal(select(store(w,u,x),v),select(w,v)) ),
file('SWV507-1.030.p',unknown),
[] ).
cnf(136,plain,
equal(select(a_1075,n7),e7),
inference(spr,[status(thm),theory(equality)],[9,1]),
[iquote('0:SpR:9.0,1.0')] ).
cnf(135,plain,
equal(select(a_1127,n7),e7),
inference(spr,[status(thm),theory(equality)],[61,1]),
[iquote('0:SpR:61.0,1.0')] ).
cnf(134,plain,
equal(select(a_1078,n10),e10),
inference(spr,[status(thm),theory(equality)],[12,1]),
[iquote('0:SpR:12.0,1.0')] ).
cnf(133,plain,
equal(select(a_1128,n10),e10),
inference(spr,[status(thm),theory(equality)],[62,1]),
[iquote('0:SpR:62.0,1.0')] ).
cnf(1,axiom,
equal(select(store(u,v,w),v),w),
file('SWV507-1.030.p',unknown),
[] ).
cnf(3,axiom,
equal(store(a1,n1,e1),a_1069),
file('SWV507-1.030.p',unknown),
[] ).
cnf(4,axiom,
equal(store(a_1069,n2,e2),a_1070),
file('SWV507-1.030.p',unknown),
[] ).
cnf(5,axiom,
equal(store(a_1070,n3,e3),a_1071),
file('SWV507-1.030.p',unknown),
[] ).
cnf(6,axiom,
equal(store(a_1071,n4,e4),a_1072),
file('SWV507-1.030.p',unknown),
[] ).
cnf(7,axiom,
equal(store(a_1072,n5,e5),a_1073),
file('SWV507-1.030.p',unknown),
[] ).
cnf(8,axiom,
equal(store(a_1073,n6,e6),a_1074),
file('SWV507-1.030.p',unknown),
[] ).
cnf(9,axiom,
equal(store(a_1074,n7,e7),a_1075),
file('SWV507-1.030.p',unknown),
[] ).
cnf(10,axiom,
equal(store(a_1075,n8,e8),a_1076),
file('SWV507-1.030.p',unknown),
[] ).
cnf(11,axiom,
equal(store(a_1076,n9,e9),a_1077),
file('SWV507-1.030.p',unknown),
[] ).
cnf(12,axiom,
equal(store(a_1077,n10,e10),a_1078),
file('SWV507-1.030.p',unknown),
[] ).
cnf(13,axiom,
equal(store(a_1078,n11,e11),a_1079),
file('SWV507-1.030.p',unknown),
[] ).
cnf(14,axiom,
equal(store(a_1079,n12,e12),a_1080),
file('SWV507-1.030.p',unknown),
[] ).
cnf(15,axiom,
equal(store(a_1080,n13,e13),a_1081),
file('SWV507-1.030.p',unknown),
[] ).
cnf(16,axiom,
equal(store(a_1081,n14,e14),a_1082),
file('SWV507-1.030.p',unknown),
[] ).
cnf(17,axiom,
equal(store(a_1082,n15,e15),a_1083),
file('SWV507-1.030.p',unknown),
[] ).
cnf(18,axiom,
equal(store(a_1083,n16,e16),a_1084),
file('SWV507-1.030.p',unknown),
[] ).
cnf(19,axiom,
equal(store(a_1084,n17,e17),a_1085),
file('SWV507-1.030.p',unknown),
[] ).
cnf(20,axiom,
equal(store(a_1085,n18,e18),a_1086),
file('SWV507-1.030.p',unknown),
[] ).
cnf(21,axiom,
equal(store(a_1086,n19,e19),a_1087),
file('SWV507-1.030.p',unknown),
[] ).
cnf(22,axiom,
equal(store(a_1087,n20,e20),a_1088),
file('SWV507-1.030.p',unknown),
[] ).
cnf(23,axiom,
equal(store(a_1088,n21,e21),a_1089),
file('SWV507-1.030.p',unknown),
[] ).
cnf(24,axiom,
equal(store(a_1089,n22,e22),a_1090),
file('SWV507-1.030.p',unknown),
[] ).
cnf(25,axiom,
equal(store(a_1090,n23,e23),a_1091),
file('SWV507-1.030.p',unknown),
[] ).
cnf(26,axiom,
equal(store(a_1091,n24,e24),a_1092),
file('SWV507-1.030.p',unknown),
[] ).
cnf(27,axiom,
equal(store(a_1092,n25,e25),a_1093),
file('SWV507-1.030.p',unknown),
[] ).
cnf(28,axiom,
equal(store(a_1093,n26,e26),a_1094),
file('SWV507-1.030.p',unknown),
[] ).
cnf(29,axiom,
equal(store(a_1094,n27,e27),a_1095),
file('SWV507-1.030.p',unknown),
[] ).
cnf(30,axiom,
equal(store(a_1095,n28,e28),a_1096),
file('SWV507-1.030.p',unknown),
[] ).
cnf(31,axiom,
equal(store(a_1096,n29,e29),a_1097),
file('SWV507-1.030.p',unknown),
[] ).
cnf(33,axiom,
equal(store(a1,n13,e13),a_1099),
file('SWV507-1.030.p',unknown),
[] ).
cnf(34,axiom,
equal(store(a_1099,n1,e1),a_1100),
file('SWV507-1.030.p',unknown),
[] ).
cnf(35,axiom,
equal(store(a_1100,n19,e19),a_1101),
file('SWV507-1.030.p',unknown),
[] ).
cnf(36,axiom,
equal(store(a_1101,n4,e4),a_1102),
file('SWV507-1.030.p',unknown),
[] ).
cnf(37,axiom,
equal(store(a_1102,n9,e9),a_1103),
file('SWV507-1.030.p',unknown),
[] ).
cnf(39,axiom,
equal(store(a_1104,n2,e2),a_1105),
file('SWV507-1.030.p',unknown),
[] ).
cnf(40,axiom,
equal(store(a_1105,n15,e15),a_1106),
file('SWV507-1.030.p',unknown),
[] ).
cnf(41,axiom,
equal(store(a_1106,n25,e25),a_1107),
file('SWV507-1.030.p',unknown),
[] ).
cnf(42,axiom,
equal(store(a_1107,n18,e18),a_1108),
file('SWV507-1.030.p',unknown),
[] ).
cnf(43,axiom,
equal(store(a_1108,n20,e20),a_1109),
file('SWV507-1.030.p',unknown),
[] ).
cnf(44,axiom,
equal(store(a_1109,n8,e8),a_1110),
file('SWV507-1.030.p',unknown),
[] ).
cnf(45,axiom,
equal(store(a_1110,n21,e21),a_1111),
file('SWV507-1.030.p',unknown),
[] ).
cnf(46,axiom,
equal(store(a_1111,n6,e6),a_1112),
file('SWV507-1.030.p',unknown),
[] ).
cnf(47,axiom,
equal(store(a_1112,n11,e11),a_1113),
file('SWV507-1.030.p',unknown),
[] ).
cnf(48,axiom,
equal(store(a_1113,n14,e14),a_1114),
file('SWV507-1.030.p',unknown),
[] ).
cnf(49,axiom,
equal(store(a_1114,n29,e29),a_1115),
file('SWV507-1.030.p',unknown),
[] ).
cnf(50,axiom,
equal(store(a_1115,n5,e5),a_1116),
file('SWV507-1.030.p',unknown),
[] ).
cnf(51,axiom,
equal(store(a_1116,n26,e26),a_1117),
file('SWV507-1.030.p',unknown),
[] ).
cnf(52,axiom,
equal(store(a_1117,n22,e22),a_1118),
file('SWV507-1.030.p',unknown),
[] ).
cnf(53,axiom,
equal(store(a_1118,n27,e27),a_1119),
file('SWV507-1.030.p',unknown),
[] ).
cnf(54,axiom,
equal(store(a_1119,n3,e3),a_1120),
file('SWV507-1.030.p',unknown),
[] ).
cnf(55,axiom,
equal(store(a_1120,n12,e12),a_1121),
file('SWV507-1.030.p',unknown),
[] ).
cnf(56,axiom,
equal(store(a_1121,n16,e16),a_1122),
file('SWV507-1.030.p',unknown),
[] ).
cnf(57,axiom,
equal(store(a_1122,n28,e28),a_1123),
file('SWV507-1.030.p',unknown),
[] ).
cnf(58,axiom,
equal(store(a_1123,n17,e17),a_1124),
file('SWV507-1.030.p',unknown),
[] ).
cnf(59,axiom,
equal(store(a_1124,n23,e23),a_1125),
file('SWV507-1.030.p',unknown),
[] ).
cnf(60,axiom,
equal(store(a_1125,n24,e24),a_1126),
file('SWV507-1.030.p',unknown),
[] ).
cnf(61,axiom,
equal(store(a_1126,n7,e7),a_1127),
file('SWV507-1.030.p',unknown),
[] ).
cnf(62,axiom,
equal(store(a_1127,n10,e10),a_1128),
file('SWV507-1.030.p',unknown),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : SWV507-1.030 : TPTP v8.1.0. Released v4.0.0.
% 0.04/0.14 % Command : run_spass %d %s
% 0.13/0.35 % Computer : n004.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 600
% 0.13/0.35 % DateTime : Tue Jun 14 20:57:54 EDT 2022
% 0.13/0.35 % CPUTime :
% 0.21/0.50
% 0.21/0.50 SPASS V 3.9
% 0.21/0.50 SPASS beiseite: Completion found.
% 0.21/0.50 % SZS status CounterSatisfiable
% 0.21/0.50 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.21/0.50 SPASS derived 413 clauses, backtracked 0 clauses, performed 2 splits and kept 208 clauses.
% 0.21/0.50 SPASS allocated 63523 KBytes.
% 0.21/0.50 SPASS spent 0:00:00.14 on the problem.
% 0.21/0.50 0:00:00.03 for the input.
% 0.21/0.50 0:00:00.00 for the FLOTTER CNF translation.
% 0.21/0.50 0:00:00.01 for inferences.
% 0.21/0.50 0:00:00.00 for the backtracking.
% 0.21/0.50 0:00:00.06 for the reduction.
% 0.21/0.50
% 0.21/0.50
% 0.21/0.50 The saturated set of worked-off clauses is :
% 0.21/0.50 % SZS output start Saturation
% See solution above
%------------------------------------------------------------------------------