%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWV514-1.030 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %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 : 300s % DateTime : Wed Jul 27 13:20:59 EDT 2022 % Result : Unknown 3.36s 3.57s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.01/0.12 % Problem : SWV514-1.030 : TPTP v8.1.0. Released v4.0.0. % 0.01/0.12 % Command : otter-tptp-script %s % 0.12/0.33 % Computer : n004.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Wed Jul 27 05:37:36 EDT 2022 % 0.12/0.33 % CPUTime : % 1.74/1.97 ----- Otter 3.3f, August 2004 ----- % 1.74/1.97 The process was started by sandbox on n004.cluster.edu, % 1.74/1.97 Wed Jul 27 05:37:36 2022 % 1.74/1.97 The command was "./otter". The process ID is 20313. % 1.74/1.97 % 1.74/1.97 set(prolog_style_variables). % 1.74/1.97 set(auto). % 1.74/1.97 dependent: set(auto1). % 1.74/1.97 dependent: set(process_input). % 1.74/1.97 dependent: clear(print_kept). % 1.74/1.97 dependent: clear(print_new_demod). % 1.74/1.97 dependent: clear(print_back_demod). % 1.74/1.97 dependent: clear(print_back_sub). % 1.74/1.97 dependent: set(control_memory). % 1.74/1.97 dependent: assign(max_mem, 12000). % 1.74/1.97 dependent: assign(pick_given_ratio, 4). % 1.74/1.97 dependent: assign(stats_level, 1). % 1.74/1.97 dependent: assign(max_seconds, 10800). % 1.74/1.97 clear(print_given). % 1.74/1.97 % 1.74/1.97 list(usable). % 1.74/1.97 0 [] A=A. % 1.74/1.97 0 [] select(store(A,I,E),I)=E. % 1.74/1.97 0 [] I=J|select(store(A,I,E),J)=select(A,J). % 1.74/1.97 0 [] store(A,I,select(A,I))=A. % 1.74/1.97 0 [] store(store(A,I,E),I,F)=store(A,I,F). % 1.74/1.97 0 [] I=J|store(store(A,I,E),J,F)=store(store(A,J,F),I,E). % 1.74/1.97 0 [] a_1018=store(a1,n1,e1). % 1.74/1.97 0 [] a_1019=store(a_1018,n2,e2). % 1.74/1.97 0 [] a_1020=store(a_1019,n3,e3). % 1.74/1.97 0 [] a_1021=store(a_1020,n4,e4). % 1.74/1.97 0 [] a_1022=store(a_1021,n5,e5). % 1.74/1.97 0 [] a_1023=store(a_1022,n6,e6). % 1.74/1.97 0 [] a_1024=store(a_1023,n7,e7). % 1.74/1.97 0 [] a_1025=store(a_1024,n8,e8). % 1.74/1.97 0 [] a_1026=store(a_1025,n9,e9). % 1.74/1.97 0 [] a_1027=store(a_1026,n10,e10). % 1.74/1.97 0 [] a_1028=store(a_1027,n11,e11). % 1.74/1.97 0 [] a_1029=store(a_1028,n12,e12). % 1.74/1.97 0 [] a_1030=store(a_1029,n13,e13). % 1.74/1.97 0 [] a_1031=store(a_1030,n14,e14). % 1.74/1.97 0 [] a_1032=store(a_1031,n15,e15). % 1.74/1.97 0 [] a_1033=store(a_1032,n16,e16). % 1.74/1.97 0 [] a_1034=store(a_1033,n17,e17). % 1.74/1.97 0 [] a_1035=store(a_1034,n18,e18). % 1.74/1.97 0 [] a_1036=store(a_1035,n19,e19). % 1.74/1.97 0 [] a_1037=store(a_1036,n20,e20). % 1.74/1.97 0 [] a_1038=store(a_1037,n21,e21). % 1.74/1.97 0 [] a_1039=store(a_1038,n22,e22). % 1.74/1.97 0 [] a_1040=store(a_1039,n23,e23). % 1.74/1.97 0 [] a_1041=store(a_1040,n24,e24). % 1.74/1.97 0 [] a_1042=store(a_1041,n25,e25). % 1.74/1.97 0 [] a_1043=store(a_1042,n26,e26). % 1.74/1.97 0 [] a_1044=store(a_1043,n27,e27). % 1.74/1.97 0 [] a_1045=store(a_1044,n28,e28). % 1.74/1.97 0 [] a_1046=store(a_1045,n29,e29). % 1.74/1.97 0 [] a_1047=store(a_1046,n30,e30). % 1.74/1.97 0 [] a_1048=store(a1,n13,e13). % 1.74/1.97 0 [] a_1049=store(a_1048,n1,e1). % 1.74/1.97 0 [] a_1050=store(a_1049,n19,e19). % 1.74/1.97 0 [] a_1051=store(a_1050,n4,e4). % 1.74/1.97 0 [] a_1052=store(a_1051,n9,e9). % 1.74/1.97 0 [] a_1053=store(a_1052,n30,e30). % 1.74/1.97 0 [] a_1054=store(a_1053,n2,e2). % 1.74/1.97 0 [] a_1055=store(a_1054,n15,e15). % 1.74/1.97 0 [] a_1056=store(a_1055,n25,e25). % 1.74/1.97 0 [] a_1057=store(a_1056,n18,e18). % 1.74/1.97 0 [] a_1058=store(a_1057,n20,e20). % 1.74/1.97 0 [] a_1059=store(a_1058,n8,e8). % 1.74/1.97 0 [] a_1060=store(a_1059,n21,e21). % 1.74/1.97 0 [] a_1061=store(a_1060,n6,e6). % 1.74/1.97 0 [] a_1062=store(a_1061,n11,e11). % 1.74/1.97 0 [] a_1063=store(a_1062,n14,e14). % 1.74/1.97 0 [] a_1064=store(a_1063,n29,e29). % 1.74/1.97 0 [] a_1065=store(a_1064,n5,e5). % 1.74/1.97 0 [] a_1066=store(a_1065,n26,e26). % 1.74/1.97 0 [] a_1067=store(a_1066,n22,e22). % 1.74/1.97 0 [] a_1068=store(a_1067,n27,e27). % 1.74/1.97 0 [] a_1069=store(a_1068,n3,e3). % 1.74/1.97 0 [] a_1070=store(a_1069,n12,e12). % 1.74/1.97 0 [] a_1071=store(a_1070,n16,e16). % 1.74/1.97 0 [] a_1072=store(a_1071,n28,e28). % 1.74/1.97 0 [] a_1073=store(a_1072,n17,e17). % 1.74/1.97 0 [] a_1074=store(a_1073,n23,e23). % 1.74/1.97 0 [] a_1075=store(a_1074,n24,e24). % 1.74/1.97 0 [] a_1076=store(a_1075,n7,e7). % 1.74/1.97 0 [] a_1077=store(a_1076,n10,e10). % 1.74/1.97 0 [] a_1047!=a_1077. % 1.74/1.97 end_of_list. % 1.74/1.97 % 1.74/1.97 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=2. % 1.74/1.97 % 1.74/1.97 This ia a non-Horn set with equality. The strategy will be % 1.74/1.97 Knuth-Bendix, ordered hyper_res, factoring, and unit % 1.74/1.97 deletion, with positive clauses in sos and nonpositive % 1.74/1.97 clauses in usable. % 1.74/1.97 % 1.74/1.97 dependent: set(knuth_bendix). % 1.74/1.97 dependent: set(anl_eq). % 1.74/1.97 dependent: set(para_from). % 1.74/1.97 dependent: set(para_into). % 1.74/1.97 dependent: clear(para_from_right). % 1.74/1.97 dependent: clear(para_into_right). % 1.74/1.97 dependent: set(para_from_vars). % 1.74/1.97 dependent: set(eq_units_both_ways). % 1.74/1.97 dependent: set(dynamic_demod_all). % 1.74/1.97 dependent: set(dynamic_demod). % 1.74/1.97 dependent: set(order_eq). % 1.74/1.97 dependent: set(back_demod). % 1.74/1.97 dependent: set(lrpo). % 1.74/1.97 dependent: set(hyper_res). % 1.74/1.97 dependent: set(unit_deletion). % 1.74/1.97 dependent: set(factor). % 1.74/1.97 % 1.74/1.97 ------------> process usable: % 1.74/1.97 ** KEPT (pick-wt=3): 2 [copy,1,flip.1] a_1077!=a_1047. % 1.74/1.97 % 1.74/1.97 ------------> process sos: % 1.74/1.97 ** KEPT (pick-wt=3): 3 [] A=A. % 1.74/1.97 ** KEPT (pick-wt=8): 4 [] select(store(A,B,C),B)=C. % 1.74/1.97 ---> New Demodulator: 5 [new_demod,4] select(store(A,B,C),B)=C. % 1.74/1.97 ** KEPT (pick-wt=13): 6 [] A=B|select(store(C,A,D),B)=select(C,B). % 1.74/1.97 ** KEPT (pick-wt=8): 7 [] store(A,B,select(A,B))=A. % 1.74/1.97 ---> New Demodulator: 8 [new_demod,7] store(A,B,select(A,B))=A. % 1.74/1.97 ** KEPT (pick-wt=12): 9 [] store(store(A,B,C),B,D)=store(A,B,D). % 1.74/1.97 ---> New Demodulator: 10 [new_demod,9] store(store(A,B,C),B,D)=store(A,B,D). % 1.74/1.97 ** KEPT (pick-wt=18): 11 [] A=B|store(store(C,A,D),B,E)=store(store(C,B,E),A,D). % 1.74/1.97 ** KEPT (pick-wt=6): 13 [copy,12,flip.1] store(a1,n1,e1)=a_1018. % 1.74/1.97 ---> New Demodulator: 14 [new_demod,13] store(a1,n1,e1)=a_1018. % 1.74/1.97 ** KEPT (pick-wt=6): 16 [copy,15,flip.1] store(a_1018,n2,e2)=a_1019. % 1.74/1.97 ---> New Demodulator: 17 [new_demod,16] store(a_1018,n2,e2)=a_1019. % 1.74/1.97 ** KEPT (pick-wt=6): 19 [copy,18,flip.1] store(a_1019,n3,e3)=a_1020. % 1.74/1.97 ---> New Demodulator: 20 [new_demod,19] store(a_1019,n3,e3)=a_1020. % 1.74/1.97 ** KEPT (pick-wt=6): 22 [copy,21,flip.1] store(a_1020,n4,e4)=a_1021. % 1.74/1.97 ---> New Demodulator: 23 [new_demod,22] store(a_1020,n4,e4)=a_1021. % 1.74/1.97 ** KEPT (pick-wt=6): 25 [copy,24,flip.1] store(a_1021,n5,e5)=a_1022. % 1.74/1.97 ---> New Demodulator: 26 [new_demod,25] store(a_1021,n5,e5)=a_1022. % 1.74/1.97 ** KEPT (pick-wt=6): 28 [copy,27,flip.1] store(a_1022,n6,e6)=a_1023. % 1.74/1.97 ---> New Demodulator: 29 [new_demod,28] store(a_1022,n6,e6)=a_1023. % 1.74/1.97 ** KEPT (pick-wt=6): 31 [copy,30,flip.1] store(a_1023,n7,e7)=a_1024. % 1.74/1.97 ---> New Demodulator: 32 [new_demod,31] store(a_1023,n7,e7)=a_1024. % 1.74/1.97 ** KEPT (pick-wt=6): 34 [copy,33,flip.1] store(a_1024,n8,e8)=a_1025. % 1.74/1.97 ---> New Demodulator: 35 [new_demod,34] store(a_1024,n8,e8)=a_1025. % 1.74/1.97 ** KEPT (pick-wt=6): 37 [copy,36,flip.1] store(a_1025,n9,e9)=a_1026. % 1.74/1.97 ---> New Demodulator: 38 [new_demod,37] store(a_1025,n9,e9)=a_1026. % 1.74/1.97 ** KEPT (pick-wt=6): 40 [copy,39,flip.1] store(a_1026,n10,e10)=a_1027. % 1.74/1.97 ---> New Demodulator: 41 [new_demod,40] store(a_1026,n10,e10)=a_1027. % 1.74/1.97 ** KEPT (pick-wt=6): 43 [copy,42,flip.1] store(a_1027,n11,e11)=a_1028. % 1.74/1.97 ---> New Demodulator: 44 [new_demod,43] store(a_1027,n11,e11)=a_1028. % 1.74/1.97 ** KEPT (pick-wt=6): 46 [copy,45,flip.1] store(a_1028,n12,e12)=a_1029. % 1.74/1.97 ---> New Demodulator: 47 [new_demod,46] store(a_1028,n12,e12)=a_1029. % 1.74/1.97 ** KEPT (pick-wt=6): 49 [copy,48,flip.1] store(a_1029,n13,e13)=a_1030. % 1.74/1.97 ---> New Demodulator: 50 [new_demod,49] store(a_1029,n13,e13)=a_1030. % 1.74/1.97 ** KEPT (pick-wt=6): 52 [copy,51,flip.1] store(a_1030,n14,e14)=a_1031. % 1.74/1.97 ---> New Demodulator: 53 [new_demod,52] store(a_1030,n14,e14)=a_1031. % 1.74/1.97 ** KEPT (pick-wt=6): 55 [copy,54,flip.1] store(a_1031,n15,e15)=a_1032. % 1.74/1.97 ---> New Demodulator: 56 [new_demod,55] store(a_1031,n15,e15)=a_1032. % 1.74/1.97 ** KEPT (pick-wt=6): 58 [copy,57,flip.1] store(a_1032,n16,e16)=a_1033. % 1.74/1.97 ---> New Demodulator: 59 [new_demod,58] store(a_1032,n16,e16)=a_1033. % 1.74/1.97 ** KEPT (pick-wt=6): 61 [copy,60,flip.1] store(a_1033,n17,e17)=a_1034. % 1.74/1.97 ---> New Demodulator: 62 [new_demod,61] store(a_1033,n17,e17)=a_1034. % 1.74/1.97 ** KEPT (pick-wt=6): 64 [copy,63,flip.1] store(a_1034,n18,e18)=a_1035. % 1.74/1.97 ---> New Demodulator: 65 [new_demod,64] store(a_1034,n18,e18)=a_1035. % 1.74/1.97 ** KEPT (pick-wt=6): 67 [copy,66,flip.1] store(a_1035,n19,e19)=a_1036. % 1.74/1.97 ---> New Demodulator: 68 [new_demod,67] store(a_1035,n19,e19)=a_1036. % 1.74/1.97 ** KEPT (pick-wt=6): 70 [copy,69,flip.1] store(a_1036,n20,e20)=a_1037. % 1.74/1.97 ---> New Demodulator: 71 [new_demod,70] store(a_1036,n20,e20)=a_1037. % 1.74/1.97 ** KEPT (pick-wt=6): 73 [copy,72,flip.1] store(a_1037,n21,e21)=a_1038. % 1.74/1.97 ---> New Demodulator: 74 [new_demod,73] store(a_1037,n21,e21)=a_1038. % 1.74/1.97 ** KEPT (pick-wt=6): 76 [copy,75,flip.1] store(a_1038,n22,e22)=a_1039. % 1.74/1.97 ---> New Demodulator: 77 [new_demod,76] store(a_1038,n22,e22)=a_1039. % 1.74/1.97 ** KEPT (pick-wt=6): 79 [copy,78,flip.1] store(a_1039,n23,e23)=a_1040. % 1.74/1.97 ---> New Demodulator: 80 [new_demod,79] store(a_1039,n23,e23)=a_1040. % 1.74/1.97 ** KEPT (pick-wt=6): 82 [copy,81,flip.1] store(a_1040,n24,e24)=a_1041. % 1.74/1.97 ---> New Demodulator: 83 [new_demod,82] store(a_1040,n24,e24)=a_1041. % 1.74/1.97 ** KEPT (pick-wt=6): 85 [copy,84,flip.1] store(a_1041,n25,e25)=a_1042. % 1.74/1.97 ---> New Demodulator: 86 [new_demod,85] store(a_1041,n25,e25)=a_1042. % 1.74/1.97 ** KEPT (pick-wt=6): 88 [copy,87,flip.1] store(a_1042,n26,e26)=a_1043. % 1.74/1.97 ---> New Demodulator: 89 [new_demod,88] store(a_1042,n26,e26)=a_1043. % 1.74/1.97 ** KEPT (pick-wt=6): 91 [copy,90,flip.1] store(a_1043,n27,e27)=a_1044. % 1.74/1.97 ---> New Demodulator: 92 [new_demod,91] store(a_1043,n27,e27)=a_1044. % 1.74/1.97 ** KEPT (pick-wt=6): 94 [copy,93,flip.1] store(a_1044,n28,e28)=a_1045. % 1.74/1.97 ---> New Demodulator: 95 [new_demod,94] store(a_1044,n28,e28)=a_1045. % 1.74/1.97 ** KEPT (pick-wt=6): 97 [copy,96,flip.1] store(a_1045,n29,e29)=a_1046. % 1.74/1.97 ---> New Demodulator: 98 [new_demod,97] store(a_1045,n29,e29)=a_1046. % 1.74/1.97 ** KEPT (pick-wt=6): 100 [copy,99,flip.1] store(a_1046,n30,e30)=a_1047. % 1.74/1.97 ---> New Demodulator: 101 [new_demod,100] store(a_1046,n30,e30)=a_1047. % 1.74/1.97 ** KEPT (pick-wt=6): 103 [copy,102,flip.1] store(a1,n13,e13)=a_1048. % 1.74/1.97 ---> New Demodulator: 104 [new_demod,103] store(a1,n13,e13)=a_1048. % 1.74/1.97 ** KEPT (pick-wt=6): 106 [copy,105,flip.1] store(a_1048,n1,e1)=a_1049. % 1.74/1.97 ---> New Demodulator: 107 [new_demod,106] store(a_1048,n1,e1)=a_1049. % 1.74/1.97 ** KEPT (pick-wt=6): 109 [copy,108,flip.1] store(a_1049,n19,e19)=a_1050. % 1.74/1.97 ---> New Demodulator: 110 [new_demod,109] store(a_1049,n19,e19)=a_1050. % 1.74/1.97 ** KEPT (pick-wt=6): 112 [copy,111,flip.1] store(a_1050,n4,e4)=a_1051. % 1.74/1.97 ---> New Demodulator: 113 [new_demod,112] store(a_1050,n4,e4)=a_1051. % 1.74/1.97 ** KEPT (pick-wt=6): 115 [copy,114,flip.1] store(a_1051,n9,e9)=a_1052. % 1.74/1.97 ---> New Demodulator: 116 [new_demod,115] store(a_1051,n9,e9)=a_1052. % 1.74/1.97 ** KEPT (pick-wt=6): 118 [copy,117,flip.1] store(a_1052,n30,e30)=a_1053. % 1.74/1.97 ---> New Demodulator: 119 [new_demod,118] store(a_1052,n30,e30)=a_1053. % 1.74/1.97 ** KEPT (pick-wt=6): 121 [copy,120,flip.1] store(a_1053,n2,e2)=a_1054. % 1.74/1.97 ---> New Demodulator: 122 [new_demod,121] store(a_1053,n2,e2)=a_1054. % 1.74/1.97 ** KEPT (pick-wt=6): 124 [copy,123,flip.1] store(a_1054,n15,e15)=a_1055. % 1.74/1.97 ---> New Demodulator: 125 [new_demod,124] store(a_1054,n15,e15)=a_1055. % 1.74/1.97 ** KEPT (pick-wt=6): 127 [copy,126,flip.1] store(a_1055,n25,e25)=a_1056. % 1.74/1.97 ---> New Demodulator: 128 [new_demod,127] store(a_1055,n25,e25)=a_1056. % 1.74/1.97 ** KEPT (pick-wt=6): 130 [copy,129,flip.1] store(a_1056,n18,e18)=a_1057. % 1.74/1.97 ---> New Demodulator: 131 [new_demod,130] store(a_1056,n18,e18)=a_1057. % 1.74/1.97 ** KEPT (pick-wt=6): 133 [copy,132,flip.1] store(a_1057,n20,e20)=a_1058. % 1.74/1.97 ---> New Demodulator: 134 [new_demod,133] store(a_1057,n20,e20)=a_1058. % 1.74/1.97 ** KEPT (pick-wt=6): 136 [copy,135,flip.1] store(a_1058,n8,e8)=a_1059. % 1.74/1.97 ---> New Demodulator: 137 [new_demod,136] store(a_1058,n8,e8)=a_1059. % 1.74/1.97 ** KEPT (pick-wt=6): 139 [copy,138,flip.1] store(a_1059,n21,e21)=a_1060. % 1.74/1.97 ---> New Demodulator: 140 [new_demod,139] store(a_1059,n21,e21)=a_1060. % 1.74/1.97 ** KEPT (pick-wt=6): 142 [copy,141,flip.1] store(a_1060,n6,e6)=a_1061. % 1.74/1.97 ---> New Demodulator: 143 [new_demod,142] store(a_1060,n6,e6)=a_1061. % 1.74/1.97 ** KEPT (pick-wt=6): 145 [copy,144,flip.1] store(a_1061,n11,e11)=a_1062. % 1.74/1.97 ---> New Demodulator: 146 [new_demod,145] store(a_1061,n11,e11)=a_1062. % 1.74/1.97 ** KEPT (pick-wt=6): 148 [copy,147,flip.1] store(a_1062,n14,e14)=a_1063. % 1.74/1.97 ---> New Demodulator: 149 [new_demod,148] store(a_1062,n14,e14)=a_1063. % 1.74/1.97 ** KEPT (pick-wt=6): 151 [copy,150,flip.1] store(a_1063,n29,e29)=a_1064. % 1.74/1.97 ---> New Demodulator: 152 [new_demod,151] store(a_1063,n29,e29)=a_1064. % 1.74/1.97 ** KEPT (pick-wt=6): 154 [copy,153,flip.1] store(a_1064,n5,e5)=a_1065. % 1.74/1.97 ---> New Demodulator: 155 [new_demod,154] store(a_1064,n5,e5)=a_1065. % 1.74/1.97 ** KEPT (pick-wt=6): 157 [copy,156,flip.1] store(a_1065,n26,e26)=a_1066. % 1.74/1.97 ---> New Demodulator: 158 [new_demod,157] store(a_1065,n26,e26)=a_1066. % 1.74/1.97 ** KEPT (pick-wt=6): 160 [copy,159,flip.1] store(a_1066,n22,e22)=a_1067. % 1.74/1.97 ---> New Demodulator: 161 [new_demod,160] store(a_1066,n22,e22)=a_1067. % 1.74/1.97 ** KEPT (pick-wt=6): 163 [copy,162,flip.1] store(a_1067,n27,e27)=a_1068. % 1.74/1.97 ---> New Demodulator: 164 [new_demod,163] store(a_1067,n27,e27)=a_1068. % 1.74/1.97 ** KEPT (pick-wt=6): 166 [copy,165,flip.1] store(a_1068,n3,e3)=a_1069. % 1.74/1.97 ---> New Demodulator: 167 [new_demod,166] store(a_1068,n3,e3)=a_1069. % 1.74/1.97 ** KEPT (pick-wt=6): 169 [copy,168,flip.1] store(a_1069,n12,e12)=a_1070. % 1.74/1.97 ---> New Demodulator: 170 [new_demod,169] store(a_1069,n12,e12)=a_1070. % 1.74/1.97 ** KEPT (pick-wt=6): 172 [copy,171,flip.1] store(a_1070,n16,e16)=a_1071. % 1.74/1.97 ---> New Demodulator: 173 [new_demod,172] store(a_1070,n16,e16)=a_1071. % 1.74/1.97 ** KEPT (pick-wt=6): 175 [copy,174,flip.1] store(a_1071,n28,e28)=a_1072. % 1.74/1.97 ---> New Demodulator: 176 [new_demod,175] store(a_1071,n28,e28)=a_1072. % 1.74/1.97 ** KEPT (pick-wt=6): 178 [copy,177,flip.1] store(a_1072,n17,e17)=a_1073. % 1.74/1.97 ---> New Demodulator: 179 [new_demod,178] store(a_1072,n17,e17)=a_1073. % 3.36/3.56 ** KEPT (pick-wt=6): 181 [copy,180,flip.1] store(a_1073,n23,e23)=a_1074. % 3.36/3.56 ---> New Demodulator: 182 [new_demod,181] store(a_1073,n23,e23)=a_1074. % 3.36/3.56 ** KEPT (pick-wt=6): 184 [copy,183,flip.1] store(a_1074,n24,e24)=a_1075. % 3.36/3.56 ---> New Demodulator: 185 [new_demod,184] store(a_1074,n24,e24)=a_1075. % 3.36/3.56 ** KEPT (pick-wt=6): 187 [copy,186,flip.1] store(a_1075,n7,e7)=a_1076. % 3.36/3.56 ---> New Demodulator: 188 [new_demod,187] store(a_1075,n7,e7)=a_1076. % 3.36/3.56 ** KEPT (pick-wt=6): 190 [copy,189,flip.1] store(a_1076,n10,e10)=a_1077. % 3.36/3.56 ---> New Demodulator: 191 [new_demod,190] store(a_1076,n10,e10)=a_1077. % 3.36/3.56 Following clause subsumed by 3 during input processing: 0 [copy,3,flip.1] A=A. % 3.36/3.56 >>>> Starting back demodulation with 5. % 3.36/3.56 >>>> Starting back demodulation with 8. % 3.36/3.56 >>>> Starting back demodulation with 10. % 3.36/3.56 >>>> Starting back demodulation with 14. % 3.36/3.56 >>>> Starting back demodulation with 17. % 3.36/3.56 >>>> Starting back demodulation with 20. % 3.36/3.56 >>>> Starting back demodulation with 23. % 3.36/3.56 >>>> Starting back demodulation with 26. % 3.36/3.56 >>>> Starting back demodulation with 29. % 3.36/3.56 >>>> Starting back demodulation with 32. % 3.36/3.56 >>>> Starting back demodulation with 35. % 3.36/3.56 >>>> Starting back demodulation with 38. % 3.36/3.56 >>>> Starting back demodulation with 41. % 3.36/3.56 >>>> Starting back demodulation with 44. % 3.36/3.56 >>>> Starting back demodulation with 47. % 3.36/3.56 >>>> Starting back demodulation with 50. % 3.36/3.56 >>>> Starting back demodulation with 53. % 3.36/3.56 >>>> Starting back demodulation with 56. % 3.36/3.56 >>>> Starting back demodulation with 59. % 3.36/3.56 >>>> Starting back demodulation with 62. % 3.36/3.56 >>>> Starting back demodulation with 65. % 3.36/3.56 >>>> Starting back demodulation with 68. % 3.36/3.56 >>>> Starting back demodulation with 71. % 3.36/3.56 >>>> Starting back demodulation with 74. % 3.36/3.56 >>>> Starting back demodulation with 77. % 3.36/3.56 >>>> Starting back demodulation with 80. % 3.36/3.56 >>>> Starting back demodulation with 83. % 3.36/3.56 >>>> Starting back demodulation with 86. % 3.36/3.56 >>>> Starting back demodulation with 89. % 3.36/3.56 >>>> Starting back demodulation with 92. % 3.36/3.56 >>>> Starting back demodulation with 95. % 3.36/3.56 >>>> Starting back demodulation with 98. % 3.36/3.56 >>>> Starting back demodulation with 101. % 3.36/3.56 >>>> Starting back demodulation with 104. % 3.36/3.57 >>>> Starting back demodulation with 107. % 3.36/3.57 >>>> Starting back demodulation with 110. % 3.36/3.57 >>>> Starting back demodulation with 113. % 3.36/3.57 >>>> Starting back demodulation with 116. % 3.36/3.57 >>>> Starting back demodulation with 119. % 3.36/3.57 >>>> Starting back demodulation with 122. % 3.36/3.57 >>>> Starting back demodulation with 125. % 3.36/3.57 >>>> Starting back demodulation with 128. % 3.36/3.57 >>>> Starting back demodulation with 131. % 3.36/3.57 >>>> Starting back demodulation with 134. % 3.36/3.57 >>>> Starting back demodulation with 137. % 3.36/3.57 >>>> Starting back demodulation with 140. % 3.36/3.57 >>>> Starting back demodulation with 143. % 3.36/3.57 >>>> Starting back demodulation with 146. % 3.36/3.57 >>>> Starting back demodulation with 149. % 3.36/3.57 >>>> Starting back demodulation with 152. % 3.36/3.57 >>>> Starting back demodulation with 155. % 3.36/3.57 >>>> Starting back demodulation with 158. % 3.36/3.57 >>>> Starting back demodulation with 161. % 3.36/3.57 >>>> Starting back demodulation with 164. % 3.36/3.57 >>>> Starting back demodulation with 167. % 3.36/3.57 >>>> Starting back demodulation with 170. % 3.36/3.57 >>>> Starting back demodulation with 173. % 3.36/3.57 >>>> Starting back demodulation with 176. % 3.36/3.57 >>>> Starting back demodulation with 179. % 3.36/3.57 >>>> Starting back demodulation with 182. % 3.36/3.57 >>>> Starting back demodulation with 185. % 3.36/3.57 >>>> Starting back demodulation with 188. % 3.36/3.57 >>>> Starting back demodulation with 191. % 3.36/3.57 % 3.36/3.57 ======= end of input processing ======= % 3.36/3.57 % 3.36/3.57 =========== start of search =========== % 3.36/3.57 % 3.36/3.57 % 3.36/3.57 Resetting weight limit to 6. % 3.36/3.57 % 3.36/3.57 % 3.36/3.57 Resetting weight limit to 6. % 3.36/3.57 % 3.36/3.57 sos_size=438 % 3.36/3.57 % 3.36/3.57 Search stopped because sos empty. % 3.36/3.57 % 3.36/3.57 % 3.36/3.57 Search stopped because sos empty. % 3.36/3.57 % 3.36/3.57 ============ end of search ============ % 3.36/3.57 % 3.36/3.57 -------------- statistics ------------- % 3.36/3.57 clauses given 565 % 3.36/3.57 clauses generated 241223 % 3.36/3.57 clauses kept 603 % 3.36/3.57 clauses forward subsumed 817 % 3.36/3.57 clauses back subsumed 29 % 3.36/3.57 Kbytes malloced 6835 % 3.36/3.57 % 3.36/3.57 ----------- times (seconds) ----------- % 3.36/3.57 user CPU time 1.60 (0 hr, 0 min, 1 sec) % 3.36/3.57 system CPU time 0.00 (0 hr, 0 min, 0 sec) % 3.36/3.57 wall-clock time 3 (0 hr, 0 min, 3 sec) % 3.36/3.57 % 3.36/3.57 Process 20313 finished Wed Jul 27 05:37:39 2022 % 3.36/3.57 Otter interrupted % 3.36/3.57 PROOF NOT FOUND %------------------------------------------------------------------------------