%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWV540-1.010 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n010.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 : 300s % DateTime : Wed Jul 27 13:21:06 EDT 2022 % Result : Unknown 45.65s 45.85s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWV540-1.010 : TPTP v8.1.0. Released v4.0.0. % 0.07/0.13 % Command : otter-tptp-script %s % 0.12/0.34 % Computer : n010.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Wed Jul 27 05:45:10 EDT 2022 % 0.12/0.34 % CPUTime : % 1.81/2.00 ----- Otter 3.3f, August 2004 ----- % 1.81/2.00 The process was started by sandbox2 on n010.cluster.edu, % 1.81/2.00 Wed Jul 27 05:45:10 2022 % 1.81/2.00 The command was "./otter". The process ID is 19648. % 1.81/2.00 % 1.81/2.00 set(prolog_style_variables). % 1.81/2.00 set(auto). % 1.81/2.00 dependent: set(auto1). % 1.81/2.00 dependent: set(process_input). % 1.81/2.00 dependent: clear(print_kept). % 1.81/2.00 dependent: clear(print_new_demod). % 1.81/2.00 dependent: clear(print_back_demod). % 1.81/2.00 dependent: clear(print_back_sub). % 1.81/2.00 dependent: set(control_memory). % 1.81/2.00 dependent: assign(max_mem, 12000). % 1.81/2.00 dependent: assign(pick_given_ratio, 4). % 1.81/2.00 dependent: assign(stats_level, 1). % 1.81/2.00 dependent: assign(max_seconds, 10800). % 1.81/2.00 clear(print_given). % 1.81/2.00 % 1.81/2.00 list(usable). % 1.81/2.00 0 [] A=A. % 1.81/2.00 0 [] select(store(A,I,E),I)=E. % 1.81/2.00 0 [] I=J|select(store(A,I,E),J)=select(A,J). % 1.81/2.00 0 [] store(A,I,select(A,I))=A. % 1.81/2.00 0 [] store(store(A,I,E),I,F)=store(A,I,F). % 1.81/2.00 0 [] I=J|store(store(A,I,E),J,F)=store(store(A,J,F),I,E). % 1.81/2.00 0 [] a_1245=store(a1,i8,e_1244). % 1.81/2.00 0 [] a_1247=store(a_1245,i7,e_1246). % 1.81/2.00 0 [] a_1249=store(a_1247,i6,e_1248). % 1.81/2.00 0 [] a_1251=store(a_1249,i8,e_1250). % 1.81/2.00 0 [] a_1253=store(a_1251,i8,e_1252). % 1.81/2.00 0 [] a_1255=store(a_1253,i5,e_1254). % 1.81/2.00 0 [] a_1257=store(a_1255,i4,e_1256). % 1.81/2.00 0 [] a_1259=store(a_1257,i9,e_1258). % 1.81/2.00 0 [] a_1261=store(a_1259,i7,e_1260). % 1.81/2.00 0 [] a_1263=store(a_1261,i1,e_1262). % 1.81/2.00 0 [] a_1265=store(a_1263,i4,e_1264). % 1.81/2.00 0 [] a_1267=store(a_1265,i5,e_1266). % 1.81/2.00 0 [] a_1269=store(a_1267,i0,e_1268). % 1.81/2.00 0 [] a_1270=store(a_1269,i0,e_1268). % 1.81/2.00 0 [] a_1272=store(a_1270,i1,e_1271). % 1.81/2.00 0 [] a_1274=store(a_1272,i2,e_1273). % 1.81/2.00 0 [] a_1276=store(a_1274,i3,e_1275). % 1.81/2.00 0 [] a_1278=store(a_1276,i0,e_1277). % 1.81/2.00 0 [] a_1280=store(a_1278,i9,e_1279). % 1.81/2.00 0 [] a_1282=store(a_1280,i5,e_1281). % 1.81/2.00 0 [] a_1283=store(a1,i7,e_1246). % 1.81/2.00 0 [] a_1284=store(a_1283,i8,e_1244). % 1.81/2.00 0 [] a_1286=store(a_1284,i6,e_1285). % 1.81/2.00 0 [] a_1288=store(a_1286,i8,e_1287). % 1.81/2.00 0 [] a_1290=store(a_1288,i5,e_1289). % 1.81/2.00 0 [] a_1292=store(a_1290,i8,e_1291). % 1.81/2.00 0 [] a_1294=store(a_1292,i4,e_1293). % 1.81/2.00 0 [] a_1296=store(a_1294,i9,e_1295). % 1.81/2.00 0 [] a_1298=store(a_1296,i1,e_1297). % 1.81/2.00 0 [] a_1300=store(a_1298,i7,e_1299). % 1.81/2.00 0 [] a_1302=store(a_1300,i4,e_1301). % 1.81/2.00 0 [] a_1304=store(a_1302,i5,e_1303). % 1.81/2.00 0 [] a_1306=store(a_1304,i0,e_1305). % 1.81/2.00 0 [] a_1307=store(a_1306,i0,e_1305). % 1.81/2.00 0 [] a_1309=store(a_1307,i2,e_1308). % 1.81/2.00 0 [] a_1311=store(a_1309,i1,e_1310). % 1.81/2.00 0 [] a_1313=store(a_1311,i3,e_1312). % 1.81/2.00 0 [] a_1315=store(a_1313,i0,e_1314). % 1.81/2.00 0 [] a_1317=store(a_1315,i5,e_1316). % 1.81/2.00 0 [] a_1319=store(a_1317,i9,e_1318). % 1.81/2.00 0 [] e_1244=select(a1,i7). % 1.81/2.00 0 [] e_1246=select(a1,i8). % 1.81/2.00 0 [] e_1248=select(a_1247,i8). % 1.81/2.00 0 [] e_1250=select(a_1247,i6). % 1.81/2.00 0 [] e_1252=select(a_1251,i5). % 1.81/2.00 0 [] e_1254=select(a_1251,i8). % 1.81/2.00 0 [] e_1256=select(a_1255,i9). % 1.81/2.00 0 [] e_1258=select(a_1255,i4). % 1.81/2.00 0 [] e_1260=select(a_1259,i1). % 1.81/2.00 0 [] e_1262=select(a_1259,i7). % 1.81/2.00 0 [] e_1264=select(a_1263,i5). % 1.81/2.00 0 [] e_1266=select(a_1263,i4). % 1.81/2.00 0 [] e_1268=select(a_1267,i0). % 1.81/2.00 0 [] e_1271=select(a_1270,i2). % 1.81/2.00 0 [] e_1273=select(a_1270,i1). % 1.81/2.00 0 [] e_1275=select(a_1274,i0). % 1.81/2.00 0 [] e_1277=select(a_1274,i3). % 1.81/2.00 0 [] e_1279=select(a_1278,i5). % 1.81/2.00 0 [] e_1281=select(a_1278,i9). % 1.81/2.00 0 [] e_1285=select(a_1284,i8). % 1.81/2.00 0 [] e_1287=select(a_1284,i6). % 1.81/2.00 0 [] e_1289=select(a_1288,i8). % 1.81/2.00 0 [] e_1291=select(a_1288,i5). % 1.81/2.00 0 [] e_1293=select(a_1292,i9). % 1.81/2.00 0 [] e_1295=select(a_1292,i4). % 1.81/2.00 0 [] e_1297=select(a_1296,i7). % 1.81/2.00 0 [] e_1299=select(a_1296,i1). % 1.81/2.00 0 [] e_1301=select(a_1300,i5). % 1.81/2.00 0 [] e_1303=select(a_1300,i4). % 1.81/2.00 0 [] e_1305=select(a_1304,i0). % 1.81/2.00 0 [] e_1308=select(a_1307,i1). % 1.81/2.00 0 [] e_1310=select(a_1307,i2). % 1.81/2.00 0 [] e_1312=select(a_1311,i0). % 1.81/2.00 0 [] e_1314=select(a_1311,i3). % 1.81/2.00 0 [] e_1316=select(a_1315,i9). % 1.81/2.00 0 [] e_1318=select(a_1315,i5). % 1.81/2.00 0 [] a_1282!=a_1319. % 1.81/2.00 end_of_list. % 1.81/2.00 % 1.81/2.00 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=2. % 1.81/2.00 % 1.81/2.00 This ia a non-Horn set with equality. The strategy will be % 1.81/2.00 Knuth-Bendix, ordered hyper_res, factoring, and unit % 1.81/2.00 deletion, with positive clauses in sos and nonpositive % 1.81/2.00 clauses in usable. % 1.81/2.00 % 1.81/2.00 dependent: set(knuth_bendix). % 1.81/2.00 dependent: set(anl_eq). % 1.81/2.00 dependent: set(para_from). % 1.81/2.00 dependent: set(para_into). % 1.81/2.00 dependent: clear(para_from_right). % 1.81/2.00 dependent: clear(para_into_right). % 1.81/2.00 dependent: set(para_from_vars). % 1.81/2.00 dependent: set(eq_units_both_ways). % 1.81/2.00 dependent: set(dynamic_demod_all). % 1.81/2.00 dependent: set(dynamic_demod). % 1.81/2.00 dependent: set(order_eq). % 1.81/2.00 dependent: set(back_demod). % 1.81/2.00 dependent: set(lrpo). % 1.81/2.00 dependent: set(hyper_res). % 1.81/2.00 dependent: set(unit_deletion). % 1.81/2.00 dependent: set(factor). % 1.81/2.00 % 1.81/2.00 ------------> process usable: % 1.81/2.00 ** KEPT (pick-wt=3): 2 [copy,1,flip.1] a_1319!=a_1282. % 1.81/2.00 % 1.81/2.00 ------------> process sos: % 1.81/2.00 ** KEPT (pick-wt=3): 3 [] A=A. % 1.81/2.00 ** KEPT (pick-wt=8): 4 [] select(store(A,B,C),B)=C. % 1.81/2.00 ---> New Demodulator: 5 [new_demod,4] select(store(A,B,C),B)=C. % 1.81/2.00 ** KEPT (pick-wt=13): 6 [] A=B|select(store(C,A,D),B)=select(C,B). % 1.81/2.00 ** KEPT (pick-wt=8): 7 [] store(A,B,select(A,B))=A. % 1.81/2.00 ---> New Demodulator: 8 [new_demod,7] store(A,B,select(A,B))=A. % 1.81/2.00 ** KEPT (pick-wt=12): 9 [] store(store(A,B,C),B,D)=store(A,B,D). % 1.81/2.00 ---> New Demodulator: 10 [new_demod,9] store(store(A,B,C),B,D)=store(A,B,D). % 1.81/2.00 ** KEPT (pick-wt=18): 11 [] A=B|store(store(C,A,D),B,E)=store(store(C,B,E),A,D). % 1.81/2.00 ** KEPT (pick-wt=6): 13 [copy,12,flip.1] store(a1,i8,e_1244)=a_1245. % 1.81/2.00 ---> New Demodulator: 14 [new_demod,13] store(a1,i8,e_1244)=a_1245. % 1.81/2.00 ** KEPT (pick-wt=6): 16 [copy,15,flip.1] store(a_1245,i7,e_1246)=a_1247. % 1.81/2.00 ---> New Demodulator: 17 [new_demod,16] store(a_1245,i7,e_1246)=a_1247. % 1.81/2.00 ** KEPT (pick-wt=6): 19 [copy,18,flip.1] store(a_1247,i6,e_1248)=a_1249. % 1.81/2.00 ---> New Demodulator: 20 [new_demod,19] store(a_1247,i6,e_1248)=a_1249. % 1.81/2.00 ** KEPT (pick-wt=6): 22 [copy,21,flip.1] store(a_1249,i8,e_1250)=a_1251. % 1.81/2.00 ---> New Demodulator: 23 [new_demod,22] store(a_1249,i8,e_1250)=a_1251. % 1.81/2.00 ** KEPT (pick-wt=6): 25 [copy,24,flip.1] store(a_1251,i8,e_1252)=a_1253. % 1.81/2.00 ---> New Demodulator: 26 [new_demod,25] store(a_1251,i8,e_1252)=a_1253. % 1.81/2.00 ** KEPT (pick-wt=6): 28 [copy,27,flip.1] store(a_1253,i5,e_1254)=a_1255. % 1.81/2.00 ---> New Demodulator: 29 [new_demod,28] store(a_1253,i5,e_1254)=a_1255. % 1.81/2.00 ** KEPT (pick-wt=6): 31 [copy,30,flip.1] store(a_1255,i4,e_1256)=a_1257. % 1.81/2.00 ---> New Demodulator: 32 [new_demod,31] store(a_1255,i4,e_1256)=a_1257. % 1.81/2.00 ** KEPT (pick-wt=6): 34 [copy,33,flip.1] store(a_1257,i9,e_1258)=a_1259. % 1.81/2.00 ---> New Demodulator: 35 [new_demod,34] store(a_1257,i9,e_1258)=a_1259. % 1.81/2.00 ** KEPT (pick-wt=6): 37 [copy,36,flip.1] store(a_1259,i7,e_1260)=a_1261. % 1.81/2.00 ---> New Demodulator: 38 [new_demod,37] store(a_1259,i7,e_1260)=a_1261. % 1.81/2.00 ** KEPT (pick-wt=6): 40 [copy,39,flip.1] store(a_1261,i1,e_1262)=a_1263. % 1.81/2.00 ---> New Demodulator: 41 [new_demod,40] store(a_1261,i1,e_1262)=a_1263. % 1.81/2.00 ** KEPT (pick-wt=6): 43 [copy,42,flip.1] store(a_1263,i4,e_1264)=a_1265. % 1.81/2.00 ---> New Demodulator: 44 [new_demod,43] store(a_1263,i4,e_1264)=a_1265. % 1.81/2.00 ** KEPT (pick-wt=6): 46 [copy,45,flip.1] store(a_1265,i5,e_1266)=a_1267. % 1.81/2.00 ---> New Demodulator: 47 [new_demod,46] store(a_1265,i5,e_1266)=a_1267. % 1.81/2.00 ** KEPT (pick-wt=6): 49 [copy,48,flip.1] store(a_1267,i0,e_1268)=a_1269. % 1.81/2.00 ---> New Demodulator: 50 [new_demod,49] store(a_1267,i0,e_1268)=a_1269. % 1.81/2.00 ** KEPT (pick-wt=6): 52 [copy,51,flip.1] store(a_1269,i0,e_1268)=a_1270. % 1.81/2.00 ---> New Demodulator: 53 [new_demod,52] store(a_1269,i0,e_1268)=a_1270. % 1.81/2.00 ** KEPT (pick-wt=6): 55 [copy,54,flip.1] store(a_1270,i1,e_1271)=a_1272. % 1.81/2.00 ---> New Demodulator: 56 [new_demod,55] store(a_1270,i1,e_1271)=a_1272. % 1.81/2.00 ** KEPT (pick-wt=6): 58 [copy,57,flip.1] store(a_1272,i2,e_1273)=a_1274. % 1.81/2.00 ---> New Demodulator: 59 [new_demod,58] store(a_1272,i2,e_1273)=a_1274. % 1.81/2.00 ** KEPT (pick-wt=6): 61 [copy,60,flip.1] store(a_1274,i3,e_1275)=a_1276. % 1.81/2.00 ---> New Demodulator: 62 [new_demod,61] store(a_1274,i3,e_1275)=a_1276. % 1.81/2.00 ** KEPT (pick-wt=6): 64 [copy,63,flip.1] store(a_1276,i0,e_1277)=a_1278. % 1.81/2.00 ---> New Demodulator: 65 [new_demod,64] store(a_1276,i0,e_1277)=a_1278. % 1.81/2.00 ** KEPT (pick-wt=6): 67 [copy,66,flip.1] store(a_1278,i9,e_1279)=a_1280. % 1.81/2.00 ---> New Demodulator: 68 [new_demod,67] store(a_1278,i9,e_1279)=a_1280. % 1.81/2.00 ** KEPT (pick-wt=6): 70 [copy,69,flip.1] store(a_1280,i5,e_1281)=a_1282. % 1.81/2.00 ---> New Demodulator: 71 [new_demod,70] store(a_1280,i5,e_1281)=a_1282. % 1.81/2.00 ** KEPT (pick-wt=6): 73 [copy,72,flip.1] store(a1,i7,e_1246)=a_1283. % 1.81/2.00 ---> New Demodulator: 74 [new_demod,73] store(a1,i7,e_1246)=a_1283. % 1.81/2.00 ** KEPT (pick-wt=6): 76 [copy,75,flip.1] store(a_1283,i8,e_1244)=a_1284. % 1.81/2.00 ---> New Demodulator: 77 [new_demod,76] store(a_1283,i8,e_1244)=a_1284. % 1.81/2.00 ** KEPT (pick-wt=6): 79 [copy,78,flip.1] store(a_1284,i6,e_1285)=a_1286. % 1.81/2.00 ---> New Demodulator: 80 [new_demod,79] store(a_1284,i6,e_1285)=a_1286. % 1.81/2.00 ** KEPT (pick-wt=6): 82 [copy,81,flip.1] store(a_1286,i8,e_1287)=a_1288. % 1.81/2.00 ---> New Demodulator: 83 [new_demod,82] store(a_1286,i8,e_1287)=a_1288. % 1.81/2.00 ** KEPT (pick-wt=6): 85 [copy,84,flip.1] store(a_1288,i5,e_1289)=a_1290. % 1.81/2.00 ---> New Demodulator: 86 [new_demod,85] store(a_1288,i5,e_1289)=a_1290. % 1.81/2.00 ** KEPT (pick-wt=6): 88 [copy,87,flip.1] store(a_1290,i8,e_1291)=a_1292. % 1.81/2.00 ---> New Demodulator: 89 [new_demod,88] store(a_1290,i8,e_1291)=a_1292. % 1.81/2.00 ** KEPT (pick-wt=6): 91 [copy,90,flip.1] store(a_1292,i4,e_1293)=a_1294. % 1.81/2.00 ---> New Demodulator: 92 [new_demod,91] store(a_1292,i4,e_1293)=a_1294. % 1.81/2.00 ** KEPT (pick-wt=6): 94 [copy,93,flip.1] store(a_1294,i9,e_1295)=a_1296. % 1.81/2.00 ---> New Demodulator: 95 [new_demod,94] store(a_1294,i9,e_1295)=a_1296. % 1.81/2.00 ** KEPT (pick-wt=6): 97 [copy,96,flip.1] store(a_1296,i1,e_1297)=a_1298. % 1.81/2.00 ---> New Demodulator: 98 [new_demod,97] store(a_1296,i1,e_1297)=a_1298. % 1.81/2.00 ** KEPT (pick-wt=6): 100 [copy,99,flip.1] store(a_1298,i7,e_1299)=a_1300. % 1.81/2.00 ---> New Demodulator: 101 [new_demod,100] store(a_1298,i7,e_1299)=a_1300. % 1.81/2.00 ** KEPT (pick-wt=6): 103 [copy,102,flip.1] store(a_1300,i4,e_1301)=a_1302. % 1.81/2.00 ---> New Demodulator: 104 [new_demod,103] store(a_1300,i4,e_1301)=a_1302. % 1.81/2.00 ** KEPT (pick-wt=6): 106 [copy,105,flip.1] store(a_1302,i5,e_1303)=a_1304. % 1.81/2.00 ---> New Demodulator: 107 [new_demod,106] store(a_1302,i5,e_1303)=a_1304. % 1.81/2.00 ** KEPT (pick-wt=6): 109 [copy,108,flip.1] store(a_1304,i0,e_1305)=a_1306. % 1.81/2.00 ---> New Demodulator: 110 [new_demod,109] store(a_1304,i0,e_1305)=a_1306. % 1.81/2.00 ** KEPT (pick-wt=6): 112 [copy,111,flip.1] store(a_1306,i0,e_1305)=a_1307. % 1.81/2.00 ---> New Demodulator: 113 [new_demod,112] store(a_1306,i0,e_1305)=a_1307. % 1.81/2.00 ** KEPT (pick-wt=6): 115 [copy,114,flip.1] store(a_1307,i2,e_1308)=a_1309. % 1.81/2.00 ---> New Demodulator: 116 [new_demod,115] store(a_1307,i2,e_1308)=a_1309. % 1.81/2.00 ** KEPT (pick-wt=6): 118 [copy,117,flip.1] store(a_1309,i1,e_1310)=a_1311. % 1.81/2.00 ---> New Demodulator: 119 [new_demod,118] store(a_1309,i1,e_1310)=a_1311. % 1.81/2.00 ** KEPT (pick-wt=6): 121 [copy,120,flip.1] store(a_1311,i3,e_1312)=a_1313. % 1.81/2.00 ---> New Demodulator: 122 [new_demod,121] store(a_1311,i3,e_1312)=a_1313. % 1.81/2.00 ** KEPT (pick-wt=6): 124 [copy,123,flip.1] store(a_1313,i0,e_1314)=a_1315. % 1.81/2.00 ---> New Demodulator: 125 [new_demod,124] store(a_1313,i0,e_1314)=a_1315. % 1.81/2.00 ** KEPT (pick-wt=6): 127 [copy,126,flip.1] store(a_1315,i5,e_1316)=a_1317. % 1.81/2.00 ---> New Demodulator: 128 [new_demod,127] store(a_1315,i5,e_1316)=a_1317. % 1.81/2.00 ** KEPT (pick-wt=6): 130 [copy,129,flip.1] store(a_1317,i9,e_1318)=a_1319. % 1.81/2.00 ---> New Demodulator: 131 [new_demod,130] store(a_1317,i9,e_1318)=a_1319. % 1.81/2.00 ** KEPT (pick-wt=5): 133 [copy,132,flip.1] select(a1,i7)=e_1244. % 1.81/2.00 ---> New Demodulator: 134 [new_demod,133] select(a1,i7)=e_1244. % 1.81/2.00 ** KEPT (pick-wt=5): 136 [copy,135,flip.1] select(a1,i8)=e_1246. % 1.81/2.00 ---> New Demodulator: 137 [new_demod,136] select(a1,i8)=e_1246. % 1.81/2.00 ** KEPT (pick-wt=5): 139 [copy,138,flip.1] select(a_1247,i8)=e_1248. % 1.81/2.00 ---> New Demodulator: 140 [new_demod,139] select(a_1247,i8)=e_1248. % 1.81/2.00 ** KEPT (pick-wt=5): 142 [copy,141,flip.1] select(a_1247,i6)=e_1250. % 1.81/2.00 ---> New Demodulator: 143 [new_demod,142] select(a_1247,i6)=e_1250. % 1.81/2.00 ** KEPT (pick-wt=5): 145 [copy,144,flip.1] select(a_1251,i5)=e_1252. % 1.81/2.00 ---> New Demodulator: 146 [new_demod,145] select(a_1251,i5)=e_1252. % 1.81/2.00 ** KEPT (pick-wt=5): 148 [copy,147,flip.1] select(a_1251,i8)=e_1254. % 1.81/2.00 ---> New Demodulator: 149 [new_demod,148] select(a_1251,i8)=e_1254. % 1.81/2.00 ** KEPT (pick-wt=5): 151 [copy,150,flip.1] select(a_1255,i9)=e_1256. % 1.81/2.00 ---> New Demodulator: 152 [new_demod,151] select(a_1255,i9)=e_1256. % 1.81/2.00 ** KEPT (pick-wt=5): 154 [copy,153,flip.1] select(a_1255,i4)=e_1258. % 1.81/2.00 ---> New Demodulator: 155 [new_demod,154] select(a_1255,i4)=e_1258. % 1.81/2.00 ** KEPT (pick-wt=5): 157 [copy,156,flip.1] select(a_1259,i1)=e_1260. % 1.81/2.00 ---> New Demodulator: 158 [new_demod,157] select(a_1259,i1)=e_1260. % 1.81/2.00 ** KEPT (pick-wt=5): 160 [copy,159,flip.1] select(a_1259,i7)=e_1262. % 1.81/2.00 ---> New Demodulator: 161 [new_demod,160] select(a_1259,i7)=e_1262. % 1.81/2.00 ** KEPT (pick-wt=5): 163 [copy,162,flip.1] select(a_1263,i5)=e_1264. % 1.81/2.00 ---> New Demodulator: 164 [new_demod,163] select(a_1263,i5)=e_1264. % 1.81/2.00 ** KEPT (pick-wt=5): 166 [copy,165,flip.1] select(a_1263,i4)=e_1266. % 1.81/2.00 ---> New Demodulator: 167 [new_demod,166] select(a_1263,i4)=e_1266. % 1.81/2.00 ** KEPT (pick-wt=5): 169 [copy,168,flip.1] select(a_1267,i0)=e_1268. % 1.81/2.00 ---> New Demodulator: 170 [new_demod,169] select(a_1267,i0)=e_1268. % 1.81/2.00 ** KEPT (pick-wt=5): 172 [copy,171,flip.1] select(a_1270,i2)=e_1271. % 1.81/2.00 ---> New Demodulator: 173 [new_demod,172] select(a_1270,i2)=e_1271. % 1.81/2.00 ** KEPT (pick-wt=5): 175 [copy,174,flip.1] select(a_1270,i1)=e_1273. % 1.81/2.00 ---> New Demodulator: 176 [new_demod,175] select(a_1270,i1)=e_1273. % 1.81/2.00 ** KEPT (pick-wt=5): 178 [copy,177,flip.1] select(a_1274,i0)=e_1275. % 1.81/2.00 ---> New Demodulator: 179 [new_demod,178] select(a_1274,i0)=e_1275. % 1.81/2.00 ** KEPT (pick-wt=5): 181 [copy,180,flip.1] select(a_1274,i3)=e_1277. % 1.81/2.00 ---> New Demodulator: 182 [new_demod,181] select(a_1274,i3)=e_1277. % 1.81/2.00 ** KEPT (pick-wt=5): 184 [copy,183,flip.1] select(a_1278,i5)=e_1279. % 1.81/2.00 ---> New Demodulator: 185 [new_demod,184] select(a_1278,i5)=e_1279. % 1.81/2.00 ** KEPT (pick-wt=5): 187 [copy,186,flip.1] select(a_1278,i9)=e_1281. % 1.81/2.00 ---> New Demodulator: 188 [new_demod,187] select(a_1278,i9)=e_1281. % 1.81/2.00 ** KEPT (pick-wt=5): 190 [copy,189,flip.1] select(a_1284,i8)=e_1285. % 1.81/2.00 ---> New Demodulator: 191 [new_demod,190] select(a_1284,i8)=e_1285. % 1.81/2.00 ** KEPT (pick-wt=5): 193 [copy,192,flip.1] select(a_1284,i6)=e_1287. % 1.81/2.00 ---> New Demodulator: 194 [new_demod,193] select(a_1284,i6)=e_1287. % 1.81/2.00 ** KEPT (pick-wt=5): 196 [copy,195,flip.1] select(a_1288,i8)=e_1289. % 1.81/2.00 ---> New Demodulator: 197 [new_demod,196] select(a_1288,i8)=e_1289. % 1.81/2.00 ** KEPT (pick-wt=5): 199 [copy,198,flip.1] select(a_1288,i5)=e_1291. % 1.81/2.00 ---> New Demodulator: 200 [new_demod,199] select(a_1288,i5)=e_1291. % 1.81/2.00 ** KEPT (pick-wt=5): 202 [copy,201,flip.1] select(a_1292,i9)=e_1293. % 1.81/2.00 ---> New Demodulator: 203 [new_demod,202] select(a_1292,i9)=e_1293. % 1.81/2.00 ** KEPT (pick-wt=5): 205 [copy,204,flip.1] select(a_1292,i4)=e_1295. % 1.81/2.00 ---> New Demodulator: 206 [new_demod,205] select(a_1292,i4)=e_1295. % 1.81/2.00 ** KEPT (pick-wt=5): 208 [copy,207,flip.1] select(a_1296,i7)=e_1297. % 1.81/2.00 ---> New Demodulator: 209 [new_demod,208] select(a_1296,i7)=e_1297. % 1.81/2.00 ** KEPT (pick-wt=5): 211 [copy,210,flip.1] select(a_1296,i1)=e_1299. % 1.81/2.00 ---> New Demodulator: 212 [new_demod,211] select(a_1296,i1)=e_1299. % 1.81/2.00 ** KEPT (pick-wt=5): 214 [copy,213,flip.1] select(a_1300,i5)=e_1301. % 1.81/2.00 ---> New Demodulator: 215 [new_demod,214] select(a_1300,i5)=e_1301. % 1.81/2.00 ** KEPT (pick-wt=5): 217 [copy,216,flip.1] select(a_1300,i4)=e_1303. % 1.81/2.00 ---> New Demodulator: 218 [new_demod,217] select(a_1300,i4)=e_1303. % 1.81/2.00 ** KEPT (pick-wt=5): 220 [copy,219,flip.1] select(a_1304,i0)=e_1305. % 1.81/2.00 ---> New Demodulator: 221 [new_demod,220] select(a_1304,i0)=e_1305. % 1.81/2.00 ** KEPT (pick-wt=5): 223 [copy,222,flip.1] select(a_1307,i1)=e_1308. % 1.81/2.00 ---> New Demodulator: 224 [new_demod,223] select(a_1307,i1)=e_1308. % 1.81/2.00 ** KEPT (pick-wt=5): 226 [copy,225,flip.1] select(a_1307,i2)=e_1310. % 1.81/2.00 ---> New Demodulator: 227 [new_demod,226] select(a_1307,i2)=e_1310. % 1.81/2.00 ** KEPT (pick-wt=5): 229 [copy,228,flip.1] select(a_1311,i0)=e_1312. % 1.81/2.00 ---> New Demodulator: 230 [new_demod,229] select(a_1311,i0)=e_1312. % 1.81/2.00 ** KEPT (pick-wt=5): 232 [copy,231,flip.1] select(a_1311,i3)=e_1314. % 1.81/2.00 ---> New Demodulator: 233 [new_demod,232] select(a_1311,i3)=e_1314. % 1.81/2.00 ** KEPT (pick-wt=5): 235 [copy,234,flip.1] select(a_1315,i9)=e_1316. % 1.81/2.00 ---> New Demodulator: 236 [new_demod,235] select(a_1315,i9)=e_1316. % 1.81/2.00 ** KEPT (pick-wt=5): 238 [copy,237,flip.1] select(a_1315,i5)=e_1318. % 1.81/2.00 ---> New Demodulator: 239 [new_demod,238] select(a_1315,i5)=e_1318. % 1.81/2.00 Following clause subsumed by 3 during input processing: 0 [copy,3,flip.1] A=A. % 1.81/2.00 >>>> Starting back demodulation with 5. % 1.81/2.00 >>>> Starting back demodulation with 8. % 1.81/2.00 >>>> Starting back demodulation with 10. % 1.81/2.00 >>>> Starting back demodulation with 14. % 1.81/2.00 >>>> Starting back demodulation with 17. % 1.81/2.00 >>>> Starting back demodulation with 20. % 1.81/2.00 >>>> Starting back demodulation with 23. % 1.81/2.00 >>>> Starting back demodulation with 26. % 1.81/2.00 >>>> Starting back demodulation with 29. % 1.81/2.00 >>>> Starting back demodulation with 32. % 1.81/2.00 >>>> Starting back demodulation with 35. % 1.81/2.00 >>>> Starting back demodulation with 38. % 1.81/2.00 >>>> Starting back demodulation with 41. % 1.81/2.00 >>>> Starting back demodulation with 44. % 1.81/2.00 >>>> Starting back demodulation with 47. % 1.81/2.00 >>>> Starting back demodulation with 50. % 45.65/45.85 >>>> Starting back demodulation with 53. % 45.65/45.85 >>>> Starting back demodulation with 56. % 45.65/45.85 >>>> Starting back demodulation with 59. % 45.65/45.85 >>>> Starting back demodulation with 62. % 45.65/45.85 >>>> Starting back demodulation with 65. % 45.65/45.85 >>>> Starting back demodulation with 68. % 45.65/45.85 >>>> Starting back demodulation with 71. % 45.65/45.85 >>>> Starting back demodulation with 74. % 45.65/45.85 >>>> Starting back demodulation with 77. % 45.65/45.85 >>>> Starting back demodulation with 80. % 45.65/45.85 >>>> Starting back demodulation with 83. % 45.65/45.85 >>>> Starting back demodulation with 86. % 45.65/45.85 >>>> Starting back demodulation with 89. % 45.65/45.85 >>>> Starting back demodulation with 92. % 45.65/45.85 >>>> Starting back demodulation with 95. % 45.65/45.85 >>>> Starting back demodulation with 98. % 45.65/45.85 >>>> Starting back demodulation with 101. % 45.65/45.85 >>>> Starting back demodulation with 104. % 45.65/45.85 >>>> Starting back demodulation with 107. % 45.65/45.85 >>>> Starting back demodulation with 110. % 45.65/45.85 >>>> Starting back demodulation with 113. % 45.65/45.85 >>>> Starting back demodulation with 116. % 45.65/45.85 >>>> Starting back demodulation with 119. % 45.65/45.85 >>>> Starting back demodulation with 122. % 45.65/45.85 >>>> Starting back demodulation with 125. % 45.65/45.85 >>>> Starting back demodulation with 128. % 45.65/45.85 >>>> Starting back demodulation with 131. % 45.65/45.85 >>>> Starting back demodulation with 134. % 45.65/45.85 >>>> Starting back demodulation with 137. % 45.65/45.85 >>>> Starting back demodulation with 140. % 45.65/45.85 >>>> Starting back demodulation with 143. % 45.65/45.85 >>>> Starting back demodulation with 146. % 45.65/45.85 >>>> Starting back demodulation with 149. % 45.65/45.85 >>>> Starting back demodulation with 152. % 45.65/45.85 >>>> Starting back demodulation with 155. % 45.65/45.85 >>>> Starting back demodulation with 158. % 45.65/45.85 >>>> Starting back demodulation with 161. % 45.65/45.85 >>>> Starting back demodulation with 164. % 45.65/45.85 >>>> Starting back demodulation with 167. % 45.65/45.85 >>>> Starting back demodulation with 170. % 45.65/45.85 >>>> Starting back demodulation with 173. % 45.65/45.85 >>>> Starting back demodulation with 176. % 45.65/45.85 >>>> Starting back demodulation with 179. % 45.65/45.85 >>>> Starting back demodulation with 182. % 45.65/45.85 >>>> Starting back demodulation with 185. % 45.65/45.85 >>>> Starting back demodulation with 188. % 45.65/45.85 >>>> Starting back demodulation with 191. % 45.65/45.85 >>>> Starting back demodulation with 194. % 45.65/45.85 >>>> Starting back demodulation with 197. % 45.65/45.85 >>>> Starting back demodulation with 200. % 45.65/45.85 >>>> Starting back demodulation with 203. % 45.65/45.85 >>>> Starting back demodulation with 206. % 45.65/45.85 >>>> Starting back demodulation with 209. % 45.65/45.85 >>>> Starting back demodulation with 212. % 45.65/45.85 >>>> Starting back demodulation with 215. % 45.65/45.85 >>>> Starting back demodulation with 218. % 45.65/45.85 >>>> Starting back demodulation with 221. % 45.65/45.85 >>>> Starting back demodulation with 224. % 45.65/45.85 >>>> Starting back demodulation with 227. % 45.65/45.85 >>>> Starting back demodulation with 230. % 45.65/45.85 >>>> Starting back demodulation with 233. % 45.65/45.85 >>>> Starting back demodulation with 236. % 45.65/45.85 >>>> Starting back demodulation with 239. % 45.65/45.85 % 45.65/45.85 ======= end of input processing ======= % 45.65/45.85 % 45.65/45.85 =========== start of search =========== % 45.65/45.85 % 45.65/45.85 % 45.65/45.85 Resetting weight limit to 10. % 45.65/45.85 % 45.65/45.85 % 45.65/45.85 Resetting weight limit to 10. % 45.65/45.85 % 45.65/45.85 sos_size=1380 % 45.65/45.85 % 45.65/45.85 Search stopped in tp_alloc by max_mem option. % 45.65/45.85 % 45.65/45.85 Search stopped in tp_alloc by max_mem option. % 45.65/45.85 % 45.65/45.85 ============ end of search ============ % 45.65/45.85 % 45.65/45.85 -------------- statistics ------------- % 45.65/45.85 clauses given 2881 % 45.65/45.85 clauses generated 4950957 % 45.65/45.85 clauses kept 3792 % 45.65/45.85 clauses forward subsumed 24820 % 45.65/45.85 clauses back subsumed 105 % 45.65/45.85 Kbytes malloced 11718 % 45.65/45.85 % 45.65/45.85 ----------- times (seconds) ----------- % 45.65/45.85 user CPU time 43.83 (0 hr, 0 min, 43 sec) % 45.65/45.85 system CPU time 0.01 (0 hr, 0 min, 0 sec) % 45.65/45.85 wall-clock time 45 (0 hr, 0 min, 45 sec) % 45.65/45.85 % 45.65/45.85 Process 19648 finished Wed Jul 27 05:45:55 2022 % 45.65/45.85 Otter interrupted % 45.65/45.85 PROOF NOT FOUND %------------------------------------------------------------------------------