%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWV512-1.030 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n012.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 14.61s 14.80s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : SWV512-1.030 : TPTP v8.1.0. Released v4.0.0. % 0.10/0.12 % Command : otter-tptp-script %s % 0.12/0.33 % Computer : n012.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:52:35 EDT 2022 % 0.12/0.33 % CPUTime : % 2.33/2.52 ----- Otter 3.3f, August 2004 ----- % 2.33/2.52 The process was started by sandbox on n012.cluster.edu, % 2.33/2.52 Wed Jul 27 05:52:35 2022 % 2.33/2.52 The command was "./otter". The process ID is 9410. % 2.33/2.52 % 2.33/2.52 set(prolog_style_variables). % 2.33/2.52 set(auto). % 2.33/2.52 dependent: set(auto1). % 2.33/2.52 dependent: set(process_input). % 2.33/2.52 dependent: clear(print_kept). % 2.33/2.52 dependent: clear(print_new_demod). % 2.33/2.52 dependent: clear(print_back_demod). % 2.33/2.52 dependent: clear(print_back_sub). % 2.33/2.52 dependent: set(control_memory). % 2.33/2.52 dependent: assign(max_mem, 12000). % 2.33/2.52 dependent: assign(pick_given_ratio, 4). % 2.33/2.52 dependent: assign(stats_level, 1). % 2.33/2.52 dependent: assign(max_seconds, 10800). % 2.33/2.52 clear(print_given). % 2.33/2.52 % 2.33/2.52 list(usable). % 2.33/2.52 0 [] A=A. % 2.33/2.52 0 [] select(store(A,I,E),I)=E. % 2.33/2.52 0 [] I=J|select(store(A,I,E),J)=select(A,J). % 2.33/2.52 0 [] store(A,I,select(A,I))=A. % 2.33/2.52 0 [] store(store(A,I,E),I,F)=store(A,I,F). % 2.33/2.52 0 [] I=J|store(store(A,I,E),J,F)=store(store(A,J,F),I,E). % 2.33/2.52 0 [] a_1018=store(a1,i1,e1). % 2.33/2.52 0 [] a_1019=store(a_1018,i2,e2). % 2.33/2.52 0 [] a_1020=store(a_1019,i3,e3). % 2.33/2.52 0 [] a_1021=store(a_1020,i4,e4). % 2.33/2.52 0 [] a_1022=store(a_1021,i5,e5). % 2.33/2.52 0 [] a_1023=store(a_1022,i6,e6). % 2.33/2.52 0 [] a_1024=store(a_1023,i7,e7). % 2.33/2.52 0 [] a_1025=store(a_1024,i8,e8). % 2.33/2.52 0 [] a_1026=store(a_1025,i9,e9). % 2.33/2.52 0 [] a_1027=store(a_1026,i10,e10). % 2.33/2.52 0 [] a_1028=store(a_1027,i11,e11). % 2.33/2.52 0 [] a_1029=store(a_1028,i12,e12). % 2.33/2.52 0 [] a_1030=store(a_1029,i13,e13). % 2.33/2.52 0 [] a_1031=store(a_1030,i14,e14). % 2.33/2.52 0 [] a_1032=store(a_1031,i15,e15). % 2.33/2.52 0 [] a_1033=store(a_1032,i16,e16). % 2.33/2.52 0 [] a_1034=store(a_1033,i17,e17). % 2.33/2.52 0 [] a_1035=store(a_1034,i18,e18). % 2.33/2.52 0 [] a_1036=store(a_1035,i19,e19). % 2.33/2.52 0 [] a_1037=store(a_1036,i20,e20). % 2.33/2.52 0 [] a_1038=store(a_1037,i21,e21). % 2.33/2.52 0 [] a_1039=store(a_1038,i22,e22). % 2.33/2.52 0 [] a_1040=store(a_1039,i23,e23). % 2.33/2.52 0 [] a_1041=store(a_1040,i24,e24). % 2.33/2.52 0 [] a_1042=store(a_1041,i25,e25). % 2.33/2.52 0 [] a_1043=store(a_1042,i26,e26). % 2.33/2.52 0 [] a_1044=store(a_1043,i27,e27). % 2.33/2.52 0 [] a_1045=store(a_1044,i28,e28). % 2.33/2.52 0 [] a_1046=store(a_1045,i29,e29). % 2.33/2.52 0 [] a_1047=store(a_1046,i30,e30). % 2.33/2.52 0 [] a_1048=store(a1,i13,e13). % 2.33/2.52 0 [] a_1049=store(a_1048,i1,e1). % 2.33/2.52 0 [] a_1050=store(a_1049,i19,e19). % 2.33/2.52 0 [] a_1051=store(a_1050,i4,e4). % 2.33/2.52 0 [] a_1052=store(a_1051,i9,e9). % 2.33/2.52 0 [] a_1053=store(a_1052,i30,e30). % 2.33/2.52 0 [] a_1054=store(a_1053,i2,e2). % 2.33/2.52 0 [] a_1055=store(a_1054,i15,e15). % 2.33/2.52 0 [] a_1056=store(a_1055,i25,e25). % 2.33/2.52 0 [] a_1057=store(a_1056,i18,e18). % 2.33/2.52 0 [] a_1058=store(a_1057,i20,e20). % 2.33/2.52 0 [] a_1059=store(a_1058,i8,e8). % 2.33/2.52 0 [] a_1060=store(a_1059,i21,e21). % 2.33/2.52 0 [] a_1061=store(a_1060,i6,e6). % 2.33/2.52 0 [] a_1062=store(a_1061,i11,e11). % 2.33/2.52 0 [] a_1063=store(a_1062,i14,e14). % 2.33/2.52 0 [] a_1064=store(a_1063,i29,e29). % 2.33/2.52 0 [] a_1065=store(a_1064,i5,e5). % 2.33/2.52 0 [] a_1066=store(a_1065,i26,e26). % 2.33/2.52 0 [] a_1067=store(a_1066,i22,e22). % 2.33/2.52 0 [] a_1068=store(a_1067,i27,e27). % 2.33/2.52 0 [] a_1069=store(a_1068,i3,e3). % 2.33/2.52 0 [] a_1070=store(a_1069,i12,e12). % 2.33/2.52 0 [] a_1071=store(a_1070,i16,e16). % 2.33/2.52 0 [] a_1072=store(a_1071,i28,e28). % 2.33/2.52 0 [] a_1073=store(a_1072,i17,e17). % 2.33/2.52 0 [] a_1074=store(a_1073,i23,e23). % 2.33/2.52 0 [] a_1075=store(a_1074,i24,e24). % 2.33/2.52 0 [] a_1076=store(a_1075,i7,e7). % 2.33/2.52 0 [] a_1077=store(a_1076,i10,e10). % 2.33/2.52 0 [] i29!=i30. % 2.33/2.52 0 [] i28!=i30. % 2.33/2.52 0 [] i28!=i29. % 2.33/2.52 0 [] i27!=i30. % 2.33/2.52 0 [] i27!=i29. % 2.33/2.52 0 [] i27!=i28. % 2.33/2.52 0 [] i26!=i30. % 2.33/2.52 0 [] i26!=i29. % 2.33/2.52 0 [] i26!=i28. % 2.33/2.52 0 [] i26!=i27. % 2.33/2.52 0 [] i25!=i30. % 2.33/2.52 0 [] i25!=i29. % 2.33/2.52 0 [] i25!=i28. % 2.33/2.52 0 [] i25!=i27. % 2.33/2.52 0 [] i25!=i26. % 2.33/2.52 0 [] i24!=i30. % 2.33/2.52 0 [] i24!=i29. % 2.33/2.52 0 [] i24!=i28. % 2.33/2.52 0 [] i24!=i27. % 2.33/2.52 0 [] i24!=i26. % 2.33/2.52 0 [] i24!=i25. % 2.33/2.52 0 [] i23!=i30. % 2.33/2.52 0 [] i23!=i29. % 2.33/2.52 0 [] i23!=i28. % 2.33/2.52 0 [] i23!=i27. % 2.33/2.52 0 [] i23!=i26. % 2.33/2.52 0 [] i23!=i25. % 2.33/2.52 0 [] i23!=i24. % 2.33/2.52 0 [] i22!=i30. % 2.33/2.52 0 [] i22!=i29. % 2.33/2.52 0 [] i22!=i28. % 2.33/2.52 0 [] i22!=i27. % 2.33/2.52 0 [] i22!=i26. % 2.33/2.52 0 [] i22!=i25. % 2.33/2.52 0 [] i22!=i24. % 2.33/2.52 0 [] i22!=i23. % 2.33/2.52 0 [] i21!=i30. % 2.33/2.52 0 [] i21!=i29. % 2.33/2.52 0 [] i21!=i28. % 2.33/2.52 0 [] i21!=i27. % 2.33/2.52 0 [] i21!=i26. % 2.33/2.52 0 [] i21!=i25. % 2.33/2.52 0 [] i21!=i24. % 2.33/2.52 0 [] i21!=i23. % 2.33/2.52 0 [] i21!=i22. % 2.33/2.52 0 [] i20!=i30. % 2.33/2.52 0 [] i20!=i29. % 2.33/2.52 0 [] i20!=i28. % 2.33/2.52 0 [] i20!=i27. % 2.33/2.52 0 [] i20!=i26. % 2.33/2.52 0 [] i20!=i25. % 2.33/2.52 0 [] i20!=i24. % 2.33/2.52 0 [] i20!=i23. % 2.33/2.52 0 [] i20!=i22. % 2.33/2.52 0 [] i20!=i21. % 2.33/2.52 0 [] i19!=i30. % 2.33/2.52 0 [] i19!=i29. % 2.33/2.52 0 [] i19!=i28. % 2.33/2.52 0 [] i19!=i27. % 2.33/2.52 0 [] i19!=i26. % 2.33/2.52 0 [] i19!=i25. % 2.33/2.52 0 [] i19!=i24. % 2.33/2.52 0 [] i19!=i23. % 2.33/2.52 0 [] i19!=i22. % 2.33/2.52 0 [] i19!=i21. % 2.33/2.52 0 [] i19!=i20. % 2.33/2.52 0 [] i18!=i30. % 2.33/2.52 0 [] i18!=i29. % 2.33/2.52 0 [] i18!=i28. % 2.33/2.52 0 [] i18!=i27. % 2.33/2.52 0 [] i18!=i26. % 2.33/2.52 0 [] i18!=i25. % 2.33/2.52 0 [] i18!=i24. % 2.33/2.52 0 [] i18!=i23. % 2.33/2.52 0 [] i18!=i22. % 2.33/2.52 0 [] i18!=i21. % 2.33/2.52 0 [] i18!=i20. % 2.33/2.52 0 [] i18!=i19. % 2.33/2.52 0 [] i17!=i30. % 2.33/2.52 0 [] i17!=i29. % 2.33/2.52 0 [] i17!=i28. % 2.33/2.52 0 [] i17!=i27. % 2.33/2.52 0 [] i17!=i26. % 2.33/2.52 0 [] i17!=i25. % 2.33/2.52 0 [] i17!=i24. % 2.33/2.52 0 [] i17!=i23. % 2.33/2.52 0 [] i17!=i22. % 2.33/2.52 0 [] i17!=i21. % 2.33/2.52 0 [] i17!=i20. % 2.33/2.52 0 [] i17!=i19. % 2.33/2.52 0 [] i17!=i18. % 2.33/2.52 0 [] i16!=i30. % 2.33/2.52 0 [] i16!=i29. % 2.33/2.52 0 [] i16!=i28. % 2.33/2.52 0 [] i16!=i27. % 2.33/2.52 0 [] i16!=i26. % 2.33/2.52 0 [] i16!=i25. % 2.33/2.52 0 [] i16!=i24. % 2.33/2.52 0 [] i16!=i23. % 2.33/2.52 0 [] i16!=i22. % 2.33/2.52 0 [] i16!=i21. % 2.33/2.52 0 [] i16!=i20. % 2.33/2.52 0 [] i16!=i19. % 2.33/2.52 0 [] i16!=i18. % 2.33/2.52 0 [] i16!=i17. % 2.33/2.52 0 [] i15!=i30. % 2.33/2.52 0 [] i15!=i29. % 2.33/2.52 0 [] i15!=i28. % 2.33/2.52 0 [] i15!=i27. % 2.33/2.52 0 [] i15!=i26. % 2.33/2.52 0 [] i15!=i25. % 2.33/2.52 0 [] i15!=i24. % 2.33/2.52 0 [] i15!=i23. % 2.33/2.52 0 [] i15!=i22. % 2.33/2.52 0 [] i15!=i21. % 2.33/2.52 0 [] i15!=i20. % 2.33/2.52 0 [] i15!=i19. % 2.33/2.52 0 [] i15!=i18. % 2.33/2.52 0 [] i15!=i17. % 2.33/2.52 0 [] i15!=i16. % 2.33/2.52 0 [] i14!=i30. % 2.33/2.52 0 [] i14!=i29. % 2.33/2.52 0 [] i14!=i28. % 2.33/2.52 0 [] i14!=i27. % 2.33/2.52 0 [] i14!=i26. % 2.33/2.52 0 [] i14!=i25. % 2.33/2.52 0 [] i14!=i24. % 2.33/2.52 0 [] i14!=i23. % 2.33/2.52 0 [] i14!=i22. % 2.33/2.52 0 [] i14!=i21. % 2.33/2.52 0 [] i14!=i20. % 2.33/2.52 0 [] i14!=i19. % 2.33/2.52 0 [] i14!=i18. % 2.33/2.52 0 [] i14!=i17. % 2.33/2.52 0 [] i14!=i16. % 2.33/2.52 0 [] i14!=i15. % 2.33/2.52 0 [] i13!=i30. % 2.33/2.52 0 [] i13!=i29. % 2.33/2.52 0 [] i13!=i28. % 2.33/2.52 0 [] i13!=i27. % 2.33/2.52 0 [] i13!=i26. % 2.33/2.52 0 [] i13!=i25. % 2.33/2.52 0 [] i13!=i24. % 2.33/2.52 0 [] i13!=i23. % 2.33/2.52 0 [] i13!=i22. % 2.33/2.52 0 [] i13!=i21. % 2.33/2.52 0 [] i13!=i20. % 2.33/2.52 0 [] i13!=i19. % 2.33/2.52 0 [] i13!=i18. % 2.33/2.52 0 [] i13!=i17. % 2.33/2.52 0 [] i13!=i16. % 2.33/2.52 0 [] i13!=i15. % 2.33/2.52 0 [] i13!=i14. % 2.33/2.52 0 [] i12!=i30. % 2.33/2.52 0 [] i12!=i29. % 2.33/2.52 0 [] i12!=i28. % 2.33/2.52 0 [] i12!=i27. % 2.33/2.52 0 [] i12!=i26. % 2.33/2.52 0 [] i12!=i25. % 2.33/2.52 0 [] i12!=i24. % 2.33/2.52 0 [] i12!=i23. % 2.33/2.52 0 [] i12!=i22. % 2.33/2.52 0 [] i12!=i21. % 2.33/2.52 0 [] i12!=i20. % 2.33/2.52 0 [] i12!=i19. % 2.33/2.52 0 [] i12!=i18. % 2.33/2.52 0 [] i12!=i17. % 2.33/2.52 0 [] i12!=i16. % 2.33/2.52 0 [] i12!=i15. % 2.33/2.52 0 [] i12!=i14. % 2.33/2.52 0 [] i12!=i13. % 2.33/2.52 0 [] i11!=i30. % 2.33/2.52 0 [] i11!=i29. % 2.33/2.52 0 [] i11!=i28. % 2.33/2.52 0 [] i11!=i27. % 2.33/2.52 0 [] i11!=i26. % 2.33/2.52 0 [] i11!=i25. % 2.33/2.52 0 [] i11!=i24. % 2.33/2.52 0 [] i11!=i23. % 2.33/2.52 0 [] i11!=i22. % 2.33/2.52 0 [] i11!=i21. % 2.33/2.52 0 [] i11!=i20. % 2.33/2.52 0 [] i11!=i19. % 2.33/2.52 0 [] i11!=i18. % 2.33/2.52 0 [] i11!=i17. % 2.33/2.52 0 [] i11!=i16. % 2.33/2.52 0 [] i11!=i15. % 2.33/2.52 0 [] i11!=i14. % 2.33/2.52 0 [] i11!=i13. % 2.33/2.52 0 [] i11!=i12. % 2.33/2.52 0 [] i10!=i30. % 2.33/2.52 0 [] i10!=i29. % 2.33/2.52 0 [] i10!=i28. % 2.33/2.52 0 [] i10!=i27. % 2.33/2.52 0 [] i10!=i26. % 2.33/2.52 0 [] i10!=i25. % 2.33/2.52 0 [] i10!=i24. % 2.33/2.52 0 [] i10!=i23. % 2.33/2.52 0 [] i10!=i22. % 2.33/2.52 0 [] i10!=i21. % 2.33/2.52 0 [] i10!=i20. % 2.33/2.52 0 [] i10!=i19. % 2.33/2.52 0 [] i10!=i18. % 2.33/2.52 0 [] i10!=i17. % 2.33/2.52 0 [] i10!=i16. % 2.33/2.52 0 [] i10!=i15. % 2.33/2.52 0 [] i10!=i14. % 2.33/2.52 0 [] i10!=i13. % 2.33/2.52 0 [] i10!=i12. % 2.33/2.52 0 [] i10!=i11. % 2.33/2.52 0 [] i9!=i30. % 2.33/2.52 0 [] i9!=i29. % 2.33/2.52 0 [] i9!=i28. % 2.33/2.52 0 [] i9!=i27. % 2.33/2.52 0 [] i9!=i26. % 2.33/2.52 0 [] i9!=i25. % 2.33/2.52 0 [] i9!=i24. % 2.33/2.52 0 [] i9!=i23. % 2.33/2.52 0 [] i9!=i22. % 2.33/2.52 0 [] i9!=i21. % 2.33/2.52 0 [] i9!=i20. % 2.33/2.52 0 [] i9!=i19. % 2.33/2.52 0 [] i9!=i18. % 2.33/2.52 0 [] i9!=i17. % 2.33/2.52 0 [] i9!=i16. % 2.33/2.52 0 [] i9!=i15. % 2.33/2.52 0 [] i9!=i14. % 2.33/2.52 0 [] i9!=i13. % 2.33/2.52 0 [] i9!=i12. % 2.33/2.52 0 [] i9!=i11. % 2.33/2.52 0 [] i9!=i10. % 2.33/2.52 0 [] i8!=i30. % 2.33/2.52 0 [] i8!=i29. % 2.33/2.52 0 [] i8!=i28. % 2.33/2.52 0 [] i8!=i27. % 2.33/2.52 0 [] i8!=i26. % 2.33/2.52 0 [] i8!=i25. % 2.33/2.52 0 [] i8!=i24. % 2.33/2.52 0 [] i8!=i23. % 2.33/2.52 0 [] i8!=i22. % 2.33/2.52 0 [] i8!=i21. % 2.33/2.52 0 [] i8!=i20. % 2.33/2.52 0 [] i8!=i19. % 2.33/2.52 0 [] i8!=i18. % 2.33/2.52 0 [] i8!=i17. % 2.33/2.52 0 [] i8!=i16. % 2.33/2.52 0 [] i8!=i15. % 2.33/2.52 0 [] i8!=i14. % 2.33/2.52 0 [] i8!=i13. % 2.33/2.52 0 [] i8!=i12. % 2.33/2.52 0 [] i8!=i11. % 2.33/2.52 0 [] i8!=i10. % 2.33/2.52 0 [] i8!=i9. % 2.33/2.52 0 [] i7!=i30. % 2.33/2.52 0 [] i7!=i29. % 2.33/2.52 0 [] i7!=i28. % 2.33/2.52 0 [] i7!=i27. % 2.33/2.52 0 [] i7!=i26. % 2.33/2.52 0 [] i7!=i25. % 2.33/2.52 0 [] i7!=i24. % 2.33/2.52 0 [] i7!=i23. % 2.33/2.52 0 [] i7!=i22. % 2.33/2.52 0 [] i7!=i21. % 2.33/2.52 0 [] i7!=i20. % 2.33/2.52 0 [] i7!=i19. % 2.33/2.52 0 [] i7!=i18. % 2.33/2.52 0 [] i7!=i17. % 2.33/2.52 0 [] i7!=i16. % 2.33/2.52 0 [] i7!=i15. % 2.33/2.52 0 [] i7!=i14. % 2.33/2.52 0 [] i7!=i13. % 2.33/2.52 0 [] i7!=i12. % 2.33/2.52 0 [] i7!=i11. % 2.33/2.52 0 [] i7!=i10. % 2.33/2.52 0 [] i7!=i9. % 2.33/2.52 0 [] i7!=i8. % 2.33/2.52 0 [] i6!=i30. % 2.33/2.52 0 [] i6!=i29. % 2.33/2.52 0 [] i6!=i28. % 2.33/2.52 0 [] i6!=i27. % 2.33/2.52 0 [] i6!=i26. % 2.33/2.52 0 [] i6!=i25. % 2.33/2.52 0 [] i6!=i24. % 2.33/2.52 0 [] i6!=i23. % 2.33/2.52 0 [] i6!=i22. % 2.33/2.52 0 [] i6!=i21. % 2.33/2.52 0 [] i6!=i20. % 2.33/2.52 0 [] i6!=i19. % 2.33/2.52 0 [] i6!=i18. % 2.33/2.52 0 [] i6!=i17. % 2.33/2.52 0 [] i6!=i16. % 2.33/2.52 0 [] i6!=i15. % 2.33/2.52 0 [] i6!=i14. % 2.33/2.52 0 [] i6!=i13. % 2.33/2.52 0 [] i6!=i12. % 2.33/2.52 0 [] i6!=i11. % 2.33/2.52 0 [] i6!=i10. % 2.33/2.52 0 [] i6!=i9. % 2.33/2.52 0 [] i6!=i8. % 2.33/2.52 0 [] i6!=i7. % 2.33/2.52 0 [] i5!=i30. % 2.33/2.52 0 [] i5!=i29. % 2.33/2.52 0 [] i5!=i28. % 2.33/2.52 0 [] i5!=i27. % 2.33/2.52 0 [] i5!=i26. % 2.33/2.52 0 [] i5!=i25. % 2.33/2.52 0 [] i5!=i24. % 2.33/2.52 0 [] i5!=i23. % 2.33/2.52 0 [] i5!=i22. % 2.33/2.52 0 [] i5!=i21. % 2.33/2.52 0 [] i5!=i20. % 2.33/2.52 0 [] i5!=i19. % 2.33/2.52 0 [] i5!=i18. % 2.33/2.52 0 [] i5!=i17. % 2.33/2.52 0 [] i5!=i16. % 2.33/2.52 0 [] i5!=i15. % 2.33/2.52 0 [] i5!=i14. % 2.33/2.52 0 [] i5!=i13. % 2.33/2.52 0 [] i5!=i12. % 2.33/2.52 0 [] i5!=i11. % 2.33/2.52 0 [] i5!=i10. % 2.33/2.52 0 [] i5!=i9. % 2.33/2.52 0 [] i5!=i8. % 2.33/2.52 0 [] i5!=i7. % 2.33/2.52 0 [] i5!=i6. % 2.33/2.52 0 [] i4!=i30. % 2.33/2.52 0 [] i4!=i29. % 2.33/2.52 0 [] i4!=i28. % 2.33/2.52 0 [] i4!=i27. % 2.33/2.52 0 [] i4!=i26. % 2.33/2.52 0 [] i4!=i25. % 2.33/2.52 0 [] i4!=i24. % 2.33/2.52 0 [] i4!=i23. % 2.33/2.52 0 [] i4!=i22. % 2.33/2.52 0 [] i4!=i21. % 2.33/2.52 0 [] i4!=i20. % 2.33/2.52 0 [] i4!=i19. % 2.33/2.52 0 [] i4!=i18. % 2.33/2.52 0 [] i4!=i17. % 2.33/2.52 0 [] i4!=i16. % 2.33/2.52 0 [] i4!=i15. % 2.33/2.52 0 [] i4!=i14. % 2.33/2.52 0 [] i4!=i13. % 2.33/2.52 0 [] i4!=i12. % 2.33/2.52 0 [] i4!=i11. % 2.33/2.52 0 [] i4!=i10. % 2.33/2.52 0 [] i4!=i9. % 2.33/2.52 0 [] i4!=i8. % 2.33/2.52 0 [] i4!=i7. % 2.33/2.52 0 [] i4!=i6. % 2.33/2.52 0 [] i4!=i5. % 2.33/2.52 0 [] i3!=i30. % 2.33/2.52 0 [] i3!=i29. % 2.33/2.52 0 [] i3!=i28. % 2.33/2.52 0 [] i3!=i27. % 2.33/2.52 0 [] i3!=i26. % 2.33/2.52 0 [] i3!=i25. % 2.33/2.52 0 [] i3!=i24. % 2.33/2.52 0 [] i3!=i23. % 2.33/2.52 0 [] i3!=i22. % 2.33/2.52 0 [] i3!=i21. % 2.33/2.52 0 [] i3!=i20. % 2.33/2.52 0 [] i3!=i19. % 2.33/2.52 0 [] i3!=i18. % 2.33/2.52 0 [] i3!=i17. % 2.33/2.52 0 [] i3!=i16. % 2.33/2.52 0 [] i3!=i15. % 2.33/2.52 0 [] i3!=i14. % 2.33/2.52 0 [] i3!=i13. % 2.33/2.52 0 [] i3!=i12. % 2.33/2.52 0 [] i3!=i11. % 2.33/2.52 0 [] i3!=i10. % 2.33/2.52 0 [] i3!=i9. % 2.33/2.52 0 [] i3!=i8. % 2.33/2.52 0 [] i3!=i7. % 2.33/2.52 0 [] i3!=i6. % 2.33/2.52 0 [] i3!=i5. % 2.33/2.52 0 [] i3!=i4. % 2.33/2.52 0 [] i2!=i30. % 2.33/2.52 0 [] i2!=i29. % 2.33/2.52 0 [] i2!=i28. % 2.33/2.52 0 [] i2!=i27. % 2.33/2.52 0 [] i2!=i26. % 2.33/2.52 0 [] i2!=i25. % 2.33/2.52 0 [] i2!=i24. % 2.33/2.52 0 [] i2!=i23. % 2.33/2.52 0 [] i2!=i22. % 2.33/2.52 0 [] i2!=i21. % 2.33/2.52 0 [] i2!=i20. % 2.33/2.52 0 [] i2!=i19. % 2.33/2.52 0 [] i2!=i18. % 2.33/2.52 0 [] i2!=i17. % 2.33/2.52 0 [] i2!=i16. % 2.33/2.52 0 [] i2!=i15. % 2.33/2.52 0 [] i2!=i14. % 2.33/2.52 0 [] i2!=i13. % 2.33/2.52 0 [] i2!=i12. % 2.33/2.52 0 [] i2!=i11. % 2.33/2.52 0 [] i2!=i10. % 2.33/2.52 0 [] i2!=i9. % 2.33/2.52 0 [] i2!=i8. % 2.33/2.52 0 [] i2!=i7. % 2.33/2.52 0 [] i2!=i6. % 2.33/2.52 0 [] i2!=i5. % 2.33/2.52 0 [] i2!=i4. % 2.33/2.52 0 [] i2!=i3. % 2.33/2.52 0 [] i1!=i30. % 2.33/2.52 0 [] i1!=i29. % 2.33/2.52 0 [] i1!=i28. % 2.33/2.52 0 [] i1!=i27. % 2.33/2.52 0 [] i1!=i26. % 2.33/2.52 0 [] i1!=i25. % 2.33/2.52 0 [] i1!=i24. % 2.33/2.52 0 [] i1!=i23. % 2.33/2.52 0 [] i1!=i22. % 2.33/2.52 0 [] i1!=i21. % 2.33/2.52 0 [] i1!=i20. % 2.33/2.52 0 [] i1!=i19. % 2.33/2.52 0 [] i1!=i18. % 2.33/2.52 0 [] i1!=i17. % 2.33/2.52 0 [] i1!=i16. % 2.33/2.52 0 [] i1!=i15. % 2.33/2.52 0 [] i1!=i14. % 2.33/2.52 0 [] i1!=i13. % 2.33/2.52 0 [] i1!=i12. % 2.33/2.52 0 [] i1!=i11. % 2.33/2.52 0 [] i1!=i10. % 2.33/2.52 0 [] i1!=i9. % 2.33/2.52 0 [] i1!=i8. % 2.33/2.52 0 [] i1!=i7. % 2.33/2.52 0 [] i1!=i6. % 2.33/2.52 0 [] i1!=i5. % 2.33/2.52 0 [] i1!=i4. % 2.33/2.52 0 [] i1!=i3. % 2.33/2.52 0 [] i1!=i2. % 2.33/2.52 0 [] a_1047!=a_1077. % 2.33/2.52 end_of_list. % 2.33/2.52 % 2.33/2.52 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=2. % 2.33/2.52 % 2.33/2.52 This ia a non-Horn set with equality. The strategy will be % 2.33/2.52 Knuth-Bendix, ordered hyper_res, factoring, and unit % 2.33/2.52 deletion, with positive clauses in sos and nonpositive % 2.33/2.52 clauses in usable. % 2.33/2.52 % 2.33/2.52 dependent: set(knuth_bendix). % 2.33/2.52 dependent: set(anl_eq). % 2.33/2.52 dependent: set(para_from). % 2.33/2.52 dependent: set(para_into). % 2.33/2.52 dependent: clear(para_from_right). % 2.33/2.52 dependent: clear(para_into_right). % 2.33/2.52 dependent: set(para_from_vars). % 2.33/2.52 dependent: set(eq_units_both_ways). % 2.33/2.52 dependent: set(dynamic_demod_all). % 2.33/2.52 dependent: set(dynamic_demod). % 2.33/2.52 dependent: set(order_eq). % 2.33/2.52 dependent: set(back_demod). % 2.33/2.52 dependent: set(lrpo). % 2.33/2.52 dependent: set(hyper_res). % 2.33/2.52 dependent: set(unit_deletion). % 2.33/2.52 dependent: set(factor). % 2.33/2.52 % 2.33/2.52 ------------> process usable: % 2.33/2.52 ** KEPT (pick-wt=3): 2 [copy,1,flip.1] i30!=i29. % 2.33/2.52 ** KEPT (pick-wt=3): 4 [copy,3,flip.1] i30!=i28. % 2.33/2.52 ** KEPT (pick-wt=3): 6 [copy,5,flip.1] i29!=i28. % 2.33/2.52 ** KEPT (pick-wt=3): 8 [copy,7,flip.1] i30!=i27. % 2.33/2.52 ** KEPT (pick-wt=3): 10 [copy,9,flip.1] i29!=i27. % 2.33/2.52 ** KEPT (pick-wt=3): 12 [copy,11,flip.1] i28!=i27. % 2.33/2.52 ** KEPT (pick-wt=3): 14 [copy,13,flip.1] i30!=i26. % 2.33/2.52 ** KEPT (pick-wt=3): 16 [copy,15,flip.1] i29!=i26. % 2.33/2.52 ** KEPT (pick-wt=3): 18 [copy,17,flip.1] i28!=i26. % 2.33/2.52 ** KEPT (pick-wt=3): 20 [copy,19,flip.1] i27!=i26. % 2.33/2.52 ** KEPT (pick-wt=3): 22 [copy,21,flip.1] i30!=i25. % 2.33/2.52 ** KEPT (pick-wt=3): 24 [copy,23,flip.1] i29!=i25. % 2.33/2.52 ** KEPT (pick-wt=3): 26 [copy,25,flip.1] i28!=i25. % 2.33/2.52 ** KEPT (pick-wt=3): 28 [copy,27,flip.1] i27!=i25. % 2.33/2.52 ** KEPT (pick-wt=3): 30 [copy,29,flip.1] i26!=i25. % 2.33/2.52 ** KEPT (pick-wt=3): 32 [copy,31,flip.1] i30!=i24. % 2.33/2.52 ** KEPT (pick-wt=3): 34 [copy,33,flip.1] i29!=i24. % 2.33/2.52 ** KEPT (pick-wt=3): 36 [copy,35,flip.1] i28!=i24. % 2.33/2.52 ** KEPT (pick-wt=3): 38 [copy,37,flip.1] i27!=i24. % 2.33/2.52 ** KEPT (pick-wt=3): 40 [copy,39,flip.1] i26!=i24. % 2.33/2.52 ** KEPT (pick-wt=3): 42 [copy,41,flip.1] i25!=i24. % 2.33/2.52 ** KEPT (pick-wt=3): 44 [copy,43,flip.1] i30!=i23. % 2.33/2.52 ** KEPT (pick-wt=3): 46 [copy,45,flip.1] i29!=i23. % 2.33/2.52 ** KEPT (pick-wt=3): 48 [copy,47,flip.1] i28!=i23. % 2.33/2.52 ** KEPT (pick-wt=3): 50 [copy,49,flip.1] i27!=i23. % 2.33/2.52 ** KEPT (pick-wt=3): 52 [copy,51,flip.1] i26!=i23. % 2.33/2.52 ** KEPT (pick-wt=3): 54 [copy,53,flip.1] i25!=i23. % 2.33/2.52 ** KEPT (pick-wt=3): 56 [copy,55,flip.1] i24!=i23. % 2.33/2.52 ** KEPT (pick-wt=3): 58 [copy,57,flip.1] i30!=i22. % 2.33/2.52 ** KEPT (pick-wt=3): 60 [copy,59,flip.1] i29!=i22. % 2.33/2.52 ** KEPT (pick-wt=3): 62 [copy,61,flip.1] i28!=i22. % 2.33/2.52 ** KEPT (pick-wt=3): 64 [copy,63,flip.1] i27!=i22. % 2.33/2.52 ** KEPT (pick-wt=3): 66 [copy,65,flip.1] i26!=i22. % 2.33/2.52 ** KEPT (pick-wt=3): 68 [copy,67,flip.1] i25!=i22. % 2.33/2.52 ** KEPT (pick-wt=3): 70 [copy,69,flip.1] i24!=i22. % 2.33/2.52 ** KEPT (pick-wt=3): 72 [copy,71,flip.1] i23!=i22. % 2.33/2.52 ** KEPT (pick-wt=3): 74 [copy,73,flip.1] i30!=i21. % 2.33/2.52 ** KEPT (pick-wt=3): 76 [copy,75,flip.1] i29!=i21. % 2.33/2.52 ** KEPT (pick-wt=3): 78 [copy,77,flip.1] i28!=i21. % 2.33/2.52 ** KEPT (pick-wt=3): 80 [copy,79,flip.1] i27!=i21. % 2.33/2.52 ** KEPT (pick-wt=3): 82 [copy,81,flip.1] i26!=i21. % 2.33/2.52 ** KEPT (pick-wt=3): 84 [copy,83,flip.1] i25!=i21. % 2.33/2.52 ** KEPT (pick-wt=3): 86 [copy,85,flip.1] i24!=i21. % 2.33/2.52 ** KEPT (pick-wt=3): 88 [copy,87,flip.1] i23!=i21. % 2.33/2.52 ** KEPT (pick-wt=3): 90 [copy,89,flip.1] i22!=i21. % 2.33/2.52 ** KEPT (pick-wt=3): 92 [copy,91,flip.1] i30!=i20. % 2.33/2.52 ** KEPT (pick-wt=3): 94 [copy,93,flip.1] i29!=i20. % 2.33/2.52 ** KEPT (pick-wt=3): 96 [copy,95,flip.1] i28!=i20. % 2.33/2.52 ** KEPT (pick-wt=3): 98 [copy,97,flip.1] i27!=i20. % 2.33/2.52 ** KEPT (pick-wt=3): 100 [copy,99,flip.1] i26!=i20. % 2.33/2.52 ** KEPT (pick-wt=3): 102 [copy,101,flip.1] i25!=i20. % 2.33/2.52 ** KEPT (pick-wt=3): 104 [copy,103,flip.1] i24!=i20. % 2.33/2.52 ** KEPT (pick-wt=3): 106 [copy,105,flip.1] i23!=i20. % 2.33/2.52 ** KEPT (pick-wt=3): 108 [copy,107,flip.1] i22!=i20. % 2.33/2.52 ** KEPT (pick-wt=3): 110 [copy,109,flip.1] i21!=i20. % 2.33/2.52 ** KEPT (pick-wt=3): 112 [copy,111,flip.1] i30!=i19. % 2.33/2.52 ** KEPT (pick-wt=3): 114 [copy,113,flip.1] i29!=i19. % 2.33/2.52 ** KEPT (pick-wt=3): 116 [copy,115,flip.1] i28!=i19. % 2.33/2.52 ** KEPT (pick-wt=3): 118 [copy,117,flip.1] i27!=i19. % 2.33/2.52 ** KEPT (pick-wt=3): 120 [copy,119,flip.1] i26!=i19. % 2.33/2.52 ** KEPT (pick-wt=3): 122 [copy,121,flip.1] i25!=i19. % 2.33/2.52 ** KEPT (pick-wt=3): 124 [copy,123,flip.1] i24!=i19. % 2.33/2.52 ** KEPT (pick-wt=3): 126 [copy,125,flip.1] i23!=i19. % 2.33/2.52 ** KEPT (pick-wt=3): 128 [copy,127,flip.1] i22!=i19. % 2.33/2.52 ** KEPT (pick-wt=3): 130 [copy,129,flip.1] i21!=i19. % 2.33/2.52 ** KEPT (pick-wt=3): 132 [copy,131,flip.1] i20!=i19. % 2.33/2.52 ** KEPT (pick-wt=3): 134 [copy,133,flip.1] i30!=i18. % 2.33/2.52 ** KEPT (pick-wt=3): 136 [copy,135,flip.1] i29!=i18. % 2.33/2.52 ** KEPT (pick-wt=3): 138 [copy,137,flip.1] i28!=i18. % 2.33/2.52 ** KEPT (pick-wt=3): 140 [copy,139,flip.1] i27!=i18. % 2.33/2.52 ** KEPT (pick-wt=3): 142 [copy,141,flip.1] i26!=i18. % 2.33/2.52 ** KEPT (pick-wt=3): 144 [copy,143,flip.1] i25!=i18. % 2.33/2.52 ** KEPT (pick-wt=3): 146 [copy,145,flip.1] i24!=i18. % 2.33/2.52 ** KEPT (pick-wt=3): 148 [copy,147,flip.1] i23!=i18. % 2.33/2.52 ** KEPT (pick-wt=3): 150 [copy,149,flip.1] i22!=i18. % 2.33/2.52 ** KEPT (pick-wt=3): 152 [copy,151,flip.1] i21!=i18. % 2.33/2.52 ** KEPT (pick-wt=3): 154 [copy,153,flip.1] i20!=i18. % 2.33/2.52 ** KEPT (pick-wt=3): 156 [copy,155,flip.1] i19!=i18. % 2.33/2.52 ** KEPT (pick-wt=3): 158 [copy,157,flip.1] i30!=i17. % 2.33/2.52 ** KEPT (pick-wt=3): 160 [copy,159,flip.1] i29!=i17. % 2.33/2.52 ** KEPT (pick-wt=3): 162 [copy,161,flip.1] i28!=i17. % 2.33/2.52 ** KEPT (pick-wt=3): 164 [copy,163,flip.1] i27!=i17. % 2.33/2.52 ** KEPT (pick-wt=3): 166 [copy,165,flip.1] i26!=i17. % 2.33/2.52 ** KEPT (pick-wt=3): 168 [copy,167,flip.1] i25!=i17. % 2.33/2.52 ** KEPT (pick-wt=3): 170 [copy,169,flip.1] i24!=i17. % 2.33/2.52 ** KEPT (pick-wt=3): 172 [copy,171,flip.1] i23!=i17. % 2.33/2.52 ** KEPT (pick-wt=3): 174 [copy,173,flip.1] i22!=i17. % 2.33/2.52 ** KEPT (pick-wt=3): 176 [copy,175,flip.1] i21!=i17. % 2.33/2.52 ** KEPT (pick-wt=3): 178 [copy,177,flip.1] i20!=i17. % 2.33/2.52 ** KEPT (pick-wt=3): 180 [copy,179,flip.1] i19!=i17. % 2.33/2.52 ** KEPT (pick-wt=3): 182 [copy,181,flip.1] i18!=i17. % 2.33/2.52 ** KEPT (pick-wt=3): 184 [copy,183,flip.1] i30!=i16. % 2.33/2.52 ** KEPT (pick-wt=3): 186 [copy,185,flip.1] i29!=i16. % 2.33/2.52 ** KEPT (pick-wt=3): 188 [copy,187,flip.1] i28!=i16. % 2.33/2.52 ** KEPT (pick-wt=3): 190 [copy,189,flip.1] i27!=i16. % 2.33/2.52 ** KEPT (pick-wt=3): 192 [copy,191,flip.1] i26!=i16. % 2.33/2.52 ** KEPT (pick-wt=3): 194 [copy,193,flip.1] i25!=i16. % 2.33/2.52 ** KEPT (pick-wt=3): 196 [copy,195,flip.1] i24!=i16. % 2.33/2.52 ** KEPT (pick-wt=3): 198 [copy,197,flip.1] i23!=i16. % 2.33/2.52 ** KEPT (pick-wt=3): 200 [copy,199,flip.1] i22!=i16. % 2.33/2.52 ** KEPT (pick-wt=3): 202 [copy,201,flip.1] i21!=i16. % 2.33/2.52 ** KEPT (pick-wt=3): 204 [copy,203,flip.1] i20!=i16. % 2.33/2.52 ** KEPT (pick-wt=3): 206 [copy,205,flip.1] i19!=i16. % 2.33/2.52 ** KEPT (pick-wt=3): 208 [copy,207,flip.1] i18!=i16. % 2.33/2.52 ** KEPT (pick-wt=3): 210 [copy,209,flip.1] i17!=i16. % 2.33/2.52 ** KEPT (pick-wt=3): 212 [copy,211,flip.1] i30!=i15. % 2.33/2.52 ** KEPT (pick-wt=3): 214 [copy,213,flip.1] i29!=i15. % 2.33/2.52 ** KEPT (pick-wt=3): 216 [copy,215,flip.1] i28!=i15. % 2.33/2.52 ** KEPT (pick-wt=3): 218 [copy,217,flip.1] i27!=i15. % 2.33/2.52 ** KEPT (pick-wt=3): 220 [copy,219,flip.1] i26!=i15. % 2.33/2.52 ** KEPT (pick-wt=3): 222 [copy,221,flip.1] i25!=i15. % 2.33/2.52 ** KEPT (pick-wt=3): 224 [copy,223,flip.1] i24!=i15. % 2.33/2.52 ** KEPT (pick-wt=3): 226 [copy,225,flip.1] i23!=i15. % 2.33/2.52 ** KEPT (pick-wt=3): 228 [copy,227,flip.1] i22!=i15. % 2.33/2.52 ** KEPT (pick-wt=3): 230 [copy,229,flip.1] i21!=i15. % 2.33/2.52 ** KEPT (pick-wt=3): 232 [copy,231,flip.1] i20!=i15. % 2.33/2.52 ** KEPT (pick-wt=3): 234 [copy,233,flip.1] i19!=i15. % 2.33/2.52 ** KEPT (pick-wt=3): 236 [copy,235,flip.1] i18!=i15. % 2.33/2.52 ** KEPT (pick-wt=3): 238 [copy,237,flip.1] i17!=i15. % 2.33/2.52 ** KEPT (pick-wt=3): 240 [copy,239,flip.1] i16!=i15. % 2.33/2.52 ** KEPT (pick-wt=3): 242 [copy,241,flip.1] i30!=i14. % 2.33/2.52 ** KEPT (pick-wt=3): 244 [copy,243,flip.1] i29!=i14. % 2.33/2.52 ** KEPT (pick-wt=3): 246 [copy,245,flip.1] i28!=i14. % 2.33/2.52 ** KEPT (pick-wt=3): 248 [copy,247,flip.1] i27!=i14. % 2.33/2.52 ** KEPT (pick-wt=3): 250 [copy,249,flip.1] i26!=i14. % 2.33/2.52 ** KEPT (pick-wt=3): 252 [copy,251,flip.1] i25!=i14. % 2.33/2.52 ** KEPT (pick-wt=3): 254 [copy,253,flip.1] i24!=i14. % 2.33/2.52 ** KEPT (pick-wt=3): 256 [copy,255,flip.1] i23!=i14. % 2.33/2.52 ** KEPT (pick-wt=3): 258 [copy,257,flip.1] i22!=i14. % 2.33/2.52 ** KEPT (pick-wt=3): 260 [copy,259,flip.1] i21!=i14. % 2.33/2.52 ** KEPT (pick-wt=3): 262 [copy,261,flip.1] i20!=i14. % 2.33/2.52 ** KEPT (pick-wt=3): 264 [copy,263,flip.1] i19!=i14. % 2.33/2.52 ** KEPT (pick-wt=3): 266 [copy,265,flip.1] i18!=i14. % 2.33/2.52 ** KEPT (pick-wt=3): 268 [copy,267,flip.1] i17!=i14. % 2.33/2.52 ** KEPT (pick-wt=3): 270 [copy,269,flip.1] i16!=i14. % 2.33/2.52 ** KEPT (pick-wt=3): 272 [copy,271,flip.1] i15!=i14. % 2.33/2.52 ** KEPT (pick-wt=3): 274 [copy,273,flip.1] i30!=i13. % 2.33/2.52 ** KEPT (pick-wt=3): 276 [copy,275,flip.1] i29!=i13. % 2.33/2.52 ** KEPT (pick-wt=3): 278 [copy,277,flip.1] i28!=i13. % 2.33/2.52 ** KEPT (pick-wt=3): 280 [copy,279,flip.1] i27!=i13. % 2.33/2.52 ** KEPT (pick-wt=3): 282 [copy,281,flip.1] i26!=i13. % 2.33/2.52 ** KEPT (pick-wt=3): 284 [copy,283,flip.1] i25!=i13. % 2.33/2.52 ** KEPT (pick-wt=3): 286 [copy,285,flip.1] i24!=i13. % 2.33/2.52 ** KEPT (pick-wt=3): 288 [copy,287,flip.1] i23!=i13. % 2.33/2.52 ** KEPT (pick-wt=3): 290 [copy,289,flip.1] i22!=i13. % 2.33/2.52 ** KEPT (pick-wt=3): 292 [copy,291,flip.1] i21!=i13. % 2.33/2.52 ** KEPT (pick-wt=3): 294 [copy,293,flip.1] i20!=i13. % 2.33/2.52 ** KEPT (pick-wt=3): 296 [copy,295,flip.1] i19!=i13. % 2.33/2.52 ** KEPT (pick-wt=3): 298 [copy,297,flip.1] i18!=i13. % 2.33/2.52 ** KEPT (pick-wt=3): 300 [copy,299,flip.1] i17!=i13. % 2.33/2.52 ** KEPT (pick-wt=3): 302 [copy,301,flip.1] i16!=i13. % 2.33/2.52 ** KEPT (pick-wt=3): 304 [copy,303,flip.1] i15!=i13. % 2.33/2.52 ** KEPT (pick-wt=3): 306 [copy,305,flip.1] i14!=i13. % 2.33/2.52 ** KEPT (pick-wt=3): 308 [copy,307,flip.1] i30!=i12. % 2.33/2.52 ** KEPT (pick-wt=3): 310 [copy,309,flip.1] i29!=i12. % 2.33/2.52 ** KEPT (pick-wt=3): 312 [copy,311,flip.1] i28!=i12. % 2.33/2.52 ** KEPT (pick-wt=3): 314 [copy,313,flip.1] i27!=i12. % 2.33/2.52 ** KEPT (pick-wt=3): 316 [copy,315,flip.1] i26!=i12. % 2.33/2.52 ** KEPT (pick-wt=3): 318 [copy,317,flip.1] i25!=i12. % 2.33/2.52 ** KEPT (pick-wt=3): 320 [copy,319,flip.1] i24!=i12. % 2.33/2.52 ** KEPT (pick-wt=3): 322 [copy,321,flip.1] i23!=i12. % 2.33/2.52 ** KEPT (pick-wt=3): 324 [copy,323,flip.1] i22!=i12. % 2.33/2.52 ** KEPT (pick-wt=3): 326 [copy,325,flip.1] i21!=i12. % 2.33/2.52 ** KEPT (pick-wt=3): 328 [copy,327,flip.1] i20!=i12. % 2.33/2.52 ** KEPT (pick-wt=3): 330 [copy,329,flip.1] i19!=i12. % 2.33/2.52 ** KEPT (pick-wt=3): 332 [copy,331,flip.1] i18!=i12. % 2.33/2.52 ** KEPT (pick-wt=3): 334 [copy,333,flip.1] i17!=i12. % 2.33/2.52 ** KEPT (pick-wt=3): 336 [copy,335,flip.1] i16!=i12. % 2.33/2.52 ** KEPT (pick-wt=3): 338 [copy,337,flip.1] i15!=i12. % 2.33/2.52 ** KEPT (pick-wt=3): 340 [copy,339,flip.1] i14!=i12. % 2.33/2.52 ** KEPT (pick-wt=3): 342 [copy,341,flip.1] i13!=i12. % 2.33/2.52 ** KEPT (pick-wt=3): 344 [copy,343,flip.1] i30!=i11. % 2.33/2.52 ** KEPT (pick-wt=3): 346 [copy,345,flip.1] i29!=i11. % 2.33/2.52 ** KEPT (pick-wt=3): 348 [copy,347,flip.1] i28!=i11. % 2.33/2.52 ** KEPT (pick-wt=3): 350 [copy,349,flip.1] i27!=i11. % 2.33/2.52 ** KEPT (pick-wt=3): 352 [copy,351,flip.1] i26!=i11. % 2.33/2.52 ** KEPT (pick-wt=3): 354 [copy,353,flip.1] i25!=i11. % 2.33/2.52 ** KEPT (pick-wt=3): 356 [copy,355,flip.1] i24!=i11. % 2.33/2.52 ** KEPT (pick-wt=3): 358 [copy,357,flip.1] i23!=i11. % 2.33/2.52 ** KEPT (pick-wt=3): 360 [copy,359,flip.1] i22!=i11. % 2.33/2.52 ** KEPT (pick-wt=3): 362 [copy,361,flip.1] i21!=i11. % 2.33/2.52 ** KEPT (pick-wt=3): 364 [copy,363,flip.1] i20!=i11. % 2.33/2.52 ** KEPT (pick-wt=3): 366 [copy,365,flip.1] i19!=i11. % 2.33/2.52 ** KEPT (pick-wt=3): 368 [copy,367,flip.1] i18!=i11. % 2.33/2.52 ** KEPT (pick-wt=3): 370 [copy,369,flip.1] i17!=i11. % 2.33/2.52 ** KEPT (pick-wt=3): 372 [copy,371,flip.1] i16!=i11. % 2.33/2.52 ** KEPT (pick-wt=3): 374 [copy,373,flip.1] i15!=i11. % 2.33/2.52 ** KEPT (pick-wt=3): 376 [copy,375,flip.1] i14!=i11. % 2.33/2.52 ** KEPT (pick-wt=3): 378 [copy,377,flip.1] i13!=i11. % 2.33/2.52 ** KEPT (pick-wt=3): 380 [copy,379,flip.1] i12!=i11. % 2.33/2.52 ** KEPT (pick-wt=3): 382 [copy,381,flip.1] i30!=i10. % 2.33/2.52 ** KEPT (pick-wt=3): 384 [copy,383,flip.1] i29!=i10. % 2.33/2.52 ** KEPT (pick-wt=3): 386 [copy,385,flip.1] i28!=i10. % 2.33/2.52 ** KEPT (pick-wt=3): 388 [copy,387,flip.1] i27!=i10. % 2.33/2.52 ** KEPT (pick-wt=3): 390 [copy,389,flip.1] i26!=i10. % 2.33/2.52 ** KEPT (pick-wt=3): 392 [copy,391,flip.1] i25!=i10. % 2.33/2.52 ** KEPT (pick-wt=3): 394 [copy,393,flip.1] i24!=i10. % 2.33/2.52 ** KEPT (pick-wt=3): 396 [copy,395,flip.1] i23!=i10. % 2.33/2.52 ** KEPT (pick-wt=3): 398 [copy,397,flip.1] i22!=i10. % 2.33/2.52 ** KEPT (pick-wt=3): 400 [copy,399,flip.1] i21!=i10. % 2.33/2.52 ** KEPT (pick-wt=3): 402 [copy,401,flip.1] i20!=i10. % 2.33/2.52 ** KEPT (pick-wt=3): 404 [copy,403,flip.1] i19!=i10. % 2.33/2.52 ** KEPT (pick-wt=3): 406 [copy,405,flip.1] i18!=i10. % 2.33/2.52 ** KEPT (pick-wt=3): 408 [copy,407,flip.1] i17!=i10. % 2.33/2.52 ** KEPT (pick-wt=3): 410 [copy,409,flip.1] i16!=i10. % 2.33/2.52 ** KEPT (pick-wt=3): 412 [copy,411,flip.1] i15!=i10. % 2.33/2.52 ** KEPT (pick-wt=3): 414 [copy,413,flip.1] i14!=i10. % 2.33/2.52 ** KEPT (pick-wt=3): 416 [copy,415,flip.1] i13!=i10. % 2.33/2.52 ** KEPT (pick-wt=3): 418 [copy,417,flip.1] i12!=i10. % 2.33/2.52 ** KEPT (pick-wt=3): 420 [copy,419,flip.1] i11!=i10. % 2.33/2.52 ** KEPT (pick-wt=3): 421 [] i9!=i30. % 2.33/2.52 ** KEPT (pick-wt=3): 422 [] i9!=i29. % 2.33/2.52 ** KEPT (pick-wt=3): 423 [] i9!=i28. % 2.33/2.52 ** KEPT (pick-wt=3): 424 [] i9!=i27. % 2.33/2.52 ** KEPT (pick-wt=3): 425 [] i9!=i26. % 2.33/2.52 ** KEPT (pick-wt=3): 426 [] i9!=i25. % 2.33/2.52 ** KEPT (pick-wt=3): 427 [] i9!=i24. % 2.33/2.52 ** KEPT (pick-wt=3): 428 [] i9!=i23. % 2.33/2.52 ** KEPT (pick-wt=3): 429 [] i9!=i22. % 2.33/2.52 ** KEPT (pick-wt=3): 430 [] i9!=i21. % 2.33/2.52 ** KEPT (pick-wt=3): 431 [] i9!=i20. % 2.33/2.52 ** KEPT (pick-wt=3): 432 [] i9!=i19. % 2.33/2.52 ** KEPT (pick-wt=3): 433 [] i9!=i18. % 2.33/2.52 ** KEPT (pick-wt=3): 434 [] i9!=i17. % 2.33/2.52 ** KEPT (pick-wt=3): 435 [] i9!=i16. % 2.33/2.52 ** KEPT (pick-wt=3): 436 [] i9!=i15. % 2.33/2.52 ** KEPT (pick-wt=3): 437 [] i9!=i14. % 2.33/2.52 ** KEPT (pick-wt=3): 438 [] i9!=i13. % 2.33/2.52 ** KEPT (pick-wt=3): 439 [] i9!=i12. % 2.33/2.52 ** KEPT (pick-wt=3): 440 [] i9!=i11. % 2.33/2.52 ** KEPT (pick-wt=3): 441 [] i9!=i10. % 2.33/2.52 ** KEPT (pick-wt=3): 442 [] i8!=i30. % 2.33/2.52 ** KEPT (pick-wt=3): 443 [] i8!=i29. % 2.33/2.52 ** KEPT (pick-wt=3): 444 [] i8!=i28. % 2.33/2.52 ** KEPT (pick-wt=3): 445 [] i8!=i27. % 2.33/2.52 ** KEPT (pick-wt=3): 446 [] i8!=i26. % 2.33/2.52 ** KEPT (pick-wt=3): 447 [] i8!=i25. % 2.33/2.52 ** KEPT (pick-wt=3): 448 [] i8!=i24. % 2.33/2.52 ** KEPT (pick-wt=3): 449 [] i8!=i23. % 2.33/2.52 ** KEPT (pick-wt=3): 450 [] i8!=i22. % 2.33/2.52 ** KEPT (pick-wt=3): 451 [] i8!=i21. % 2.33/2.52 ** KEPT (pick-wt=3): 452 [] i8!=i20. % 2.33/2.52 ** KEPT (pick-wt=3): 453 [] i8!=i19. % 2.33/2.52 ** KEPT (pick-wt=3): 454 [] i8!=i18. % 2.33/2.52 ** KEPT (pick-wt=3): 455 [] i8!=i17. % 2.33/2.52 ** KEPT (pick-wt=3): 456 [] i8!=i16. % 2.33/2.52 ** KEPT (pick-wt=3): 457 [] i8!=i15. % 2.33/2.52 ** KEPT (pick-wt=3): 458 [] i8!=i14. % 2.33/2.52 ** KEPT (pick-wt=3): 459 [] i8!=i13. % 2.33/2.52 ** KEPT (pick-wt=3): 460 [] i8!=i12. % 2.33/2.52 ** KEPT (pick-wt=3): 461 [] i8!=i11. % 2.33/2.52 ** KEPT (pick-wt=3): 462 [] i8!=i10. % 2.33/2.52 ** KEPT (pick-wt=3): 464 [copy,463,flip.1] i9!=i8. % 2.33/2.52 ** KEPT (pick-wt=3): 465 [] i7!=i30. % 2.33/2.52 ** KEPT (pick-wt=3): 466 [] i7!=i29. % 2.33/2.52 ** KEPT (pick-wt=3): 467 [] i7!=i28. % 2.33/2.52 ** KEPT (pick-wt=3): 468 [] i7!=i27. % 2.33/2.52 ** KEPT (pick-wt=3): 469 [] i7!=i26. % 2.33/2.52 ** KEPT (pick-wt=3): 470 [] i7!=i25. % 2.33/2.52 ** KEPT (pick-wt=3): 471 [] i7!=i24. % 2.33/2.52 ** KEPT (pick-wt=3): 472 [] i7!=i23. % 2.33/2.52 ** KEPT (pick-wt=3): 473 [] i7!=i22. % 2.33/2.52 ** KEPT (pick-wt=3): 474 [] i7!=i21. % 2.33/2.52 ** KEPT (pick-wt=3): 475 [] i7!=i20. % 2.33/2.52 ** KEPT (pick-wt=3): 476 [] i7!=i19. % 2.33/2.52 ** KEPT (pick-wt=3): 477 [] i7!=i18. % 2.33/2.52 ** KEPT (pick-wt=3): 478 [] i7!=i17. % 2.33/2.52 ** KEPT (pick-wt=3): 479 [] i7!=i16. % 2.33/2.52 ** KEPT (pick-wt=3): 480 [] i7!=i15. % 2.33/2.52 ** KEPT (pick-wt=3): 481 [] i7!=i14. % 2.33/2.52 ** KEPT (pick-wt=3): 482 [] i7!=i13. % 2.33/2.52 ** KEPT (pick-wt=3): 483 [] i7!=i12. % 2.33/2.52 ** KEPT (pick-wt=3): 484 [] i7!=i11. % 2.33/2.52 ** KEPT (pick-wt=3): 485 [] i7!=i10. % 2.33/2.52 ** KEPT (pick-wt=3): 487 [copy,486,flip.1] i9!=i7. % 2.33/2.52 ** KEPT (pick-wt=3): 489 [copy,488,flip.1] i8!=i7. % 2.33/2.52 ** KEPT (pick-wt=3): 490 [] i6!=i30. % 2.33/2.52 ** KEPT (pick-wt=3): 491 [] i6!=i29. % 2.33/2.52 ** KEPT (pick-wt=3): 492 [] i6!=i28. % 2.33/2.52 ** KEPT (pick-wt=3): 493 [] i6!=i27. % 2.33/2.52 ** KEPT (pick-wt=3): 494 [] i6!=i26. % 2.33/2.52 ** KEPT (pick-wt=3): 495 [] i6!=i25. % 2.33/2.52 ** KEPT (pick-wt=3): 496 [] i6!=i24. % 2.33/2.52 ** KEPT (pick-wt=3): 497 [] i6!=i23. % 2.33/2.52 ** KEPT (pick-wt=3): 498 [] i6!=i22. % 2.33/2.52 ** KEPT (pick-wt=3): 499 [] i6!=i21. % 2.33/2.52 ** KEPT (pick-wt=3): 500 [] i6!=i20. % 2.33/2.52 ** KEPT (pick-wt=3): 501 [] i6!=i19. % 2.33/2.52 ** KEPT (pick-wt=3): 502 [] i6!=i18. % 2.33/2.52 ** KEPT (pick-wt=3): 503 [] i6!=i17. % 2.33/2.52 ** KEPT (pick-wt=3): 504 [] i6!=i16. % 2.33/2.52 ** KEPT (pick-wt=3): 505 [] i6!=i15. % 2.33/2.52 ** KEPT (pick-wt=3): 506 [] i6!=i14. % 2.33/2.52 ** KEPT (pick-wt=3): 507 [] i6!=i13. % 2.33/2.52 ** KEPT (pick-wt=3): 508 [] i6!=i12. % 2.33/2.52 ** KEPT (pick-wt=3): 509 [] i6!=i11. % 2.33/2.52 ** KEPT (pick-wt=3): 510 [] i6!=i10. % 2.33/2.52 ** KEPT (pick-wt=3): 512 [copy,511,flip.1] i9!=i6. % 2.33/2.52 ** KEPT (pick-wt=3): 514 [copy,513,flip.1] i8!=i6. % 2.33/2.52 ** KEPT (pick-wt=3): 516 [copy,515,flip.1] i7!=i6. % 2.33/2.52 ** KEPT (pick-wt=3): 517 [] i5!=i30. % 2.33/2.52 ** KEPT (pick-wt=3): 518 [] i5!=i29. % 2.33/2.52 ** KEPT (pick-wt=3): 519 [] i5!=i28. % 2.33/2.52 ** KEPT (pick-wt=3): 520 [] i5!=i27. % 2.33/2.52 ** KEPT (pick-wt=3): 521 [] i5!=i26. % 2.33/2.52 ** KEPT (pick-wt=3): 522 [] i5!=i25. % 2.33/2.52 ** KEPT (pick-wt=3): 523 [] i5!=i24. % 2.33/2.52 ** KEPT (pick-wt=3): 524 [] i5!=i23. % 2.33/2.52 ** KEPT (pick-wt=3): 525 [] i5!=i22. % 2.33/2.52 ** KEPT (pick-wt=3): 526 [] i5!=i21. % 2.33/2.52 ** KEPT (pick-wt=3): 527 [] i5!=i20. % 2.33/2.52 ** KEPT (pick-wt=3): 528 [] i5!=i19. % 2.33/2.52 ** KEPT (pick-wt=3): 529 [] i5!=i18. % 2.33/2.52 ** KEPT (pick-wt=3): 530 [] i5!=i17. % 2.33/2.52 ** KEPT (pick-wt=3): 531 [] i5!=i16. % 2.33/2.52 ** KEPT (pick-wt=3): 532 [] i5!=i15. % 2.33/2.52 ** KEPT (pick-wt=3): 533 [] i5!=i14. % 2.33/2.52 ** KEPT (pick-wt=3): 534 [] i5!=i13. % 2.33/2.52 ** KEPT (pick-wt=3): 535 [] i5!=i12. % 2.33/2.52 ** KEPT (pick-wt=3): 536 [] i5!=i11. % 2.33/2.52 ** KEPT (pick-wt=3): 537 [] i5!=i10. % 2.33/2.52 ** KEPT (pick-wt=3): 539 [copy,538,flip.1] i9!=i5. % 2.33/2.52 ** KEPT (pick-wt=3): 541 [copy,540,flip.1] i8!=i5. % 2.33/2.52 ** KEPT (pick-wt=3): 543 [copy,542,flip.1] i7!=i5. % 2.33/2.52 ** KEPT (pick-wt=3): 545 [copy,544,flip.1] i6!=i5. % 2.33/2.52 ** KEPT (pick-wt=3): 546 [] i4!=i30. % 2.33/2.52 ** KEPT (pick-wt=3): 547 [] i4!=i29. % 2.33/2.52 ** KEPT (pick-wt=3): 548 [] i4!=i28. % 2.33/2.52 ** KEPT (pick-wt=3): 549 [] i4!=i27. % 2.33/2.52 ** KEPT (pick-wt=3): 550 [] i4!=i26. % 2.33/2.52 ** KEPT (pick-wt=3): 551 [] i4!=i25. % 2.33/2.52 ** KEPT (pick-wt=3): 552 [] i4!=i24. % 2.33/2.52 ** KEPT (pick-wt=3): 553 [] i4!=i23. % 2.33/2.52 ** KEPT (pick-wt=3): 554 [] i4!=i22. % 2.33/2.52 ** KEPT (pick-wt=3): 555 [] i4!=i21. % 2.33/2.52 ** KEPT (pick-wt=3): 556 [] i4!=i20. % 2.33/2.52 ** KEPT (pick-wt=3): 557 [] i4!=i19. % 2.33/2.52 ** KEPT (pick-wt=3): 558 [] i4!=i18. % 2.33/2.52 ** KEPT (pick-wt=3): 559 [] i4!=i17. % 2.33/2.52 ** KEPT (pick-wt=3): 560 [] i4!=i16. % 2.33/2.52 ** KEPT (pick-wt=3): 561 [] i4!=i15. % 2.33/2.52 ** KEPT (pick-wt=3): 562 [] i4!=i14. % 2.33/2.52 ** KEPT (pick-wt=3): 563 [] i4!=i13. % 2.33/2.52 ** KEPT (pick-wt=3): 564 [] i4!=i12. % 2.33/2.52 ** KEPT (pick-wt=3): 565 [] i4!=i11. % 2.33/2.52 ** KEPT (pick-wt=3): 566 [] i4!=i10. % 2.33/2.52 ** KEPT (pick-wt=3): 568 [copy,567,flip.1] i9!=i4. % 2.33/2.52 ** KEPT (pick-wt=3): 570 [copy,569,flip.1] i8!=i4. % 2.33/2.52 ** KEPT (pick-wt=3): 572 [copy,571,flip.1] i7!=i4. % 2.33/2.52 ** KEPT (pick-wt=3): 574 [copy,573,flip.1] i6!=i4. % 2.33/2.52 ** KEPT (pick-wt=3): 576 [copy,575,flip.1] i5!=i4. % 2.33/2.52 ** KEPT (pick-wt=3): 578 [copy,577,flip.1] i30!=i3. % 2.33/2.52 ** KEPT (pick-wt=3): 579 [] i3!=i29. % 2.33/2.52 ** KEPT (pick-wt=3): 580 [] i3!=i28. % 2.33/2.52 ** KEPT (pick-wt=3): 581 [] i3!=i27. % 2.33/2.52 ** KEPT (pick-wt=3): 582 [] i3!=i26. % 2.33/2.52 ** KEPT (pick-wt=3): 583 [] i3!=i25. % 2.33/2.52 ** KEPT (pick-wt=3): 584 [] i3!=i24. % 2.33/2.52 ** KEPT (pick-wt=3): 585 [] i3!=i23. % 2.33/2.52 ** KEPT (pick-wt=3): 586 [] i3!=i22. % 2.33/2.52 ** KEPT (pick-wt=3): 587 [] i3!=i21. % 2.33/2.52 ** KEPT (pick-wt=3): 588 [] i3!=i20. % 2.33/2.52 ** KEPT (pick-wt=3): 589 [] i3!=i19. % 2.33/2.52 ** KEPT (pick-wt=3): 590 [] i3!=i18. % 2.33/2.52 ** KEPT (pick-wt=3): 591 [] i3!=i17. % 2.33/2.52 ** KEPT (pick-wt=3): 592 [] i3!=i16. % 2.33/2.52 ** KEPT (pick-wt=3): 593 [] i3!=i15. % 2.33/2.52 ** KEPT (pick-wt=3): 594 [] i3!=i14. % 2.33/2.52 ** KEPT (pick-wt=3): 595 [] i3!=i13. % 2.33/2.52 ** KEPT (pick-wt=3): 596 [] i3!=i12. % 2.33/2.52 ** KEPT (pick-wt=3): 597 [] i3!=i11. % 2.33/2.52 ** KEPT (pick-wt=3): 598 [] i3!=i10. % 2.33/2.52 ** KEPT (pick-wt=3): 600 [copy,599,flip.1] i9!=i3. % 2.33/2.52 ** KEPT (pick-wt=3): 602 [copy,601,flip.1] i8!=i3. % 2.33/2.52 ** KEPT (pick-wt=3): 604 [copy,603,flip.1] i7!=i3. % 2.33/2.52 ** KEPT (pick-wt=3): 606 [copy,605,flip.1] i6!=i3. % 2.33/2.52 ** KEPT (pick-wt=3): 608 [copy,607,flip.1] i5!=i3. % 2.33/2.52 ** KEPT (pick-wt=3): 610 [copy,609,flip.1] i4!=i3. % 2.33/2.52 ** KEPT (pick-wt=3): 612 [copy,611,flip.1] i30!=i2. % 2.33/2.52 ** KEPT (pick-wt=3): 614 [copy,613,flip.1] i29!=i2. % 2.33/2.52 ** KEPT (pick-wt=3): 616 [copy,615,flip.1] i28!=i2. % 2.33/2.52 ** KEPT (pick-wt=3): 618 [copy,617,flip.1] i27!=i2. % 2.33/2.52 ** KEPT (pick-wt=3): 620 [copy,619,flip.1] i26!=i2. % 2.33/2.52 ** KEPT (pick-wt=3): 622 [copy,621,flip.1] i25!=i2. % 2.33/2.52 ** KEPT (pick-wt=3): 624 [copy,623,flip.1] i24!=i2. % 2.33/2.52 ** KEPT (pick-wt=3): 626 [copy,625,flip.1] i23!=i2. % 2.33/2.52 ** KEPT (pick-wt=3): 628 [copy,627,flip.1] i22!=i2. % 2.33/2.52 ** KEPT (pick-wt=3): 630 [copy,629,flip.1] i21!=i2. % 2.33/2.52 ** KEPT (pick-wt=3): 632 [copy,631,flip.1] i20!=i2. % 2.33/2.52 ** KEPT (pick-wt=3): 633 [] i2!=i19. % 2.33/2.52 ** KEPT (pick-wt=3): 634 [] i2!=i18. % 2.33/2.52 ** KEPT (pick-wt=3): 635 [] i2!=i17. % 2.33/2.52 ** KEPT (pick-wt=3): 636 [] i2!=i16. % 2.33/2.52 ** KEPT (pick-wt=3): 637 [] i2!=i15. % 2.33/2.52 ** KEPT (pick-wt=3): 638 [] i2!=i14. % 2.33/2.52 ** KEPT (pick-wt=3): 639 [] i2!=i13. % 2.33/2.52 ** KEPT (pick-wt=3): 640 [] i2!=i12. % 2.33/2.52 ** KEPT (pick-wt=3): 641 [] i2!=i11. % 2.33/2.52 ** KEPT (pick-wt=3): 642 [] i2!=i10. % 2.33/2.52 ** KEPT (pick-wt=3): 644 [copy,643,flip.1] i9!=i2. % 2.33/2.52 ** KEPT (pick-wt=3): 646 [copy,645,flip.1] i8!=i2. % 2.33/2.52 ** KEPT (pick-wt=3): 648 [copy,647,flip.1] i7!=i2. % 2.33/2.52 ** KEPT (pick-wt=3): 650 [copy,649,flip.1] i6!=i2. % 2.33/2.52 ** KEPT (pick-wt=3): 652 [copy,651,flip.1] i5!=i2. % 2.33/2.52 ** KEPT (pick-wt=3): 654 [copy,653,flip.1] i4!=i2. % 2.33/2.52 ** KEPT (pick-wt=3): 656 [copy,655,flip.1] i3!=i2. % 2.33/2.52 ** KEPT (pick-wt=3): 658 [copy,657,flip.1] i30!=i1. % 2.33/2.52 ** KEPT (pick-wt=3): 660 [copy,659,flip.1] i29!=i1. % 2.33/2.52 ** KEPT (pick-wt=3): 662 [copy,661,flip.1] i28!=i1. % 2.33/2.52 ** KEPT (pick-wt=3): 664 [copy,663,flip.1] i27!=i1. % 2.33/2.52 ** KEPT (pick-wt=3): 666 [copy,665,flip.1] i26!=i1. % 2.33/2.52 ** KEPT (pick-wt=3): 668 [copy,667,flip.1] i25!=i1. % 2.33/2.52 ** KEPT (pick-wt=3): 670 [copy,669,flip.1] i24!=i1. % 2.33/2.52 ** KEPT (pick-wt=3): 672 [copy,671,flip.1] i23!=i1. % 2.33/2.52 ** KEPT (pick-wt=3): 674 [copy,673,flip.1] i22!=i1. % 2.33/2.52 ** KEPT (pick-wt=3): 676 [copy,675,flip.1] i21!=i1. % 2.33/2.52 ** KEPT (pick-wt=3): 678 [copy,677,flip.1] i20!=i1. % 2.33/2.52 ** KEPT (pick-wt=3): 680 [copy,679,flip.1] i19!=i1. % 2.33/2.52 ** KEPT (pick-wt=3): 682 [copy,681,flip.1] i18!=i1. % 2.33/2.52 ** KEPT (pick-wt=3): 684 [copy,683,flip.1] i17!=i1. % 2.33/2.52 ** KEPT (pick-wt=3): 686 [copy,685,flip.1] i16!=i1. % 2.33/2.52 ** KEPT (pick-wt=3): 688 [copy,687,flip.1] i15!=i1. % 2.33/2.52 ** KEPT (pick-wt=3): 690 [copy,689,flip.1] i14!=i1. % 2.33/2.52 ** KEPT (pick-wt=3): 692 [copy,691,flip.1] i13!=i1. % 2.33/2.52 ** KEPT (pick-wt=3): 694 [copy,693,flip.1] i12!=i1. % 2.33/2.52 ** KEPT (pick-wt=3): 696 [copy,695,flip.1] i11!=i1. % 2.33/2.52 ** KEPT (pick-wt=3): 698 [copy,697,flip.1] i10!=i1. % 2.33/2.52 ** KEPT (pick-wt=3): 700 [copy,699,flip.1] i9!=i1. % 2.33/2.52 ** KEPT (pick-wt=3): 702 [copy,701,flip.1] i8!=i1. % 2.33/2.52 ** KEPT (pick-wt=3): 704 [copy,703,flip.1] i7!=i1. % 2.33/2.52 ** KEPT (pick-wt=3): 706 [copy,705,flip.1] i6!=i1. % 2.33/2.52 ** KEPT (pick-wt=3): 708 [copy,707,flip.1] i5!=i1. % 2.33/2.52 ** KEPT (pick-wt=3): 710 [copy,709,flip.1] i4!=i1. % 2.33/2.52 ** KEPT (pick-wt=3): 712 [copy,711,flip.1] i3!=i1. % 2.33/2.52 ** KEPT (pick-wt=3): 714 [copy,713,flip.1] i2!=i1. % 2.33/2.52 ** KEPT (pick-wt=3): 716 [copy,715,flip.1] a_1077!=a_1047. % 2.33/2.52 % 2.33/2.52 ------------> process sos: % 2.33/2.52 ** KEPT (pick-wt=3): 717 [] A=A. % 2.33/2.52 ** KEPT (pick-wt=8): 718 [] select(store(A,B,C),B)=C. % 2.33/2.52 ---> New Demodulator: 719 [new_demod,718] select(store(A,B,C),B)=C. % 2.33/2.52 ** KEPT (pick-wt=13): 720 [] A=B|select(store(C,A,D),B)=select(C,B). % 2.33/2.52 ** KEPT (pick-wt=8): 721 [] store(A,B,select(A,B))=A. % 2.33/2.52 ---> New Demodulator: 722 [new_demod,721] store(A,B,select(A,B))=A. % 2.33/2.52 ** KEPT (pick-wt=12): 723 [] store(store(A,B,C),B,D)=store(A,B,D). % 2.33/2.52 ---> New Demodulator: 724 [new_demod,723] store(store(A,B,C),B,D)=store(A,B,D). % 2.33/2.52 ** KEPT (pick-wt=18): 725 [] A=B|store(store(C,A,D),B,E)=store(store(C,B,E),A,D). % 2.33/2.52 ** KEPT (pick-wt=6): 727 [copy,726,flip.1] store(a1,i1,e1)=a_1018. % 2.33/2.52 ---> New Demodulator: 728 [new_demod,727] store(a1,i1,e1)=a_1018. % 2.33/2.52 ** KEPT (pick-wt=6): 730 [copy,729,flip.1] store(a_1018,i2,e2)=a_1019. % 2.33/2.52 ---> New Demodulator: 731 [new_demod,730] store(a_1018,i2,e2)=a_1019. % 2.33/2.52 ** KEPT (pick-wt=6): 733 [copy,732,flip.1] store(a_1019,i3,e3)=a_1020. % 2.33/2.52 ---> New Demodulator: 734 [new_demod,733] store(a_1019,i3,e3)=a_1020. % 2.33/2.52 ** KEPT (pick-wt=6): 736 [copy,735,flip.1] store(a_1020,i4,e4)=a_1021. % 2.33/2.52 ---> New Demodulator: 737 [new_demod,736] store(a_1020,i4,e4)=a_1021. % 2.33/2.52 ** KEPT (pick-wt=6): 739 [copy,738,flip.1] store(a_1021,i5,e5)=a_1022. % 2.33/2.52 ---> New Demodulator: 740 [new_demod,739] store(a_1021,i5,e5)=a_1022. % 2.33/2.52 ** KEPT (pick-wt=6): 742 [copy,741,flip.1] store(a_1022,i6,e6)=a_1023. % 2.33/2.52 ---> New Demodulator: 743 [new_demod,742] store(a_1022,i6,e6)=a_1023. % 2.33/2.52 ** KEPT (pick-wt=6): 745 [copy,744,flip.1] store(a_1023,i7,e7)=a_1024. % 2.33/2.52 ---> New Demodulator: 746 [new_demod,745] store(a_1023,i7,e7)=a_1024. % 2.33/2.52 ** KEPT (pick-wt=6): 748 [copy,747,flip.1] store(a_1024,i8,e8)=a_1025. % 2.33/2.52 ---> New Demodulator: 749 [new_demod,748] store(a_1024,i8,e8)=a_1025. % 2.33/2.52 ** KEPT (pick-wt=6): 751 [copy,750,flip.1] store(a_1025,i9,e9)=a_1026. % 2.33/2.52 ---> New Demodulator: 752 [new_demod,751] store(a_1025,i9,e9)=a_1026. % 2.33/2.52 ** KEPT (pick-wt=6): 754 [copy,753,flip.1] store(a_1026,i10,e10)=a_1027. % 2.33/2.52 ---> New Demodulator: 755 [new_demod,754] store(a_1026,i10,e10)=a_1027. % 2.33/2.52 ** KEPT (pick-wt=6): 757 [copy,756,flip.1] store(a_1027,i11,e11)=a_1028. % 2.33/2.52 ---> New Demodulator: 758 [new_demod,757] store(a_1027,i11,e11)=a_1028. % 2.33/2.52 ** KEPT (pick-wt=6): 760 [copy,759,flip.1] store(a_1028,i12,e12)=a_1029. % 2.33/2.52 ---> New Demodulator: 761 [new_demod,760] store(a_1028,i12,e12)=a_1029. % 2.33/2.52 ** KEPT (pick-wt=6): 763 [copy,762,flip.1] store(a_1029,i13,e13)=a_1030. % 2.33/2.52 ---> New Demodulator: 764 [new_demod,763] store(a_1029,i13,e13)=a_1030. % 2.33/2.52 ** KEPT (pick-wt=6): 766 [copy,765,flip.1] store(a_1030,i14,e14)=a_1031. % 2.33/2.52 ---> New Demodulator: 767 [new_demod,766] store(a_1030,i14,e14)=a_1031. % 2.33/2.52 ** KEPT (pick-wt=6): 769 [copy,768,flip.1] store(a_1031,i15,e15)=a_1032. % 2.33/2.52 ---> New Demodulator: 770 [new_demod,769] store(a_1031,i15,e15)=a_1032. % 2.33/2.52 ** KEPT (pick-wt=6): 772 [copy,771,flip.1] store(a_1032,i16,e16)=a_1033. % 2.33/2.52 ---> New Demodulator: 773 [new_demod,772] store(a_1032,i16,e16)=a_1033. % 2.33/2.52 ** KEPT (pick-wt=6): 775 [copy,774,flip.1] store(a_1033,i17,e17)=a_1034. % 2.33/2.52 ---> New Demodulator: 776 [new_demod,775] store(a_1033,i17,e17)=a_1034. % 2.33/2.52 ** KEPT (pick-wt=6): 778 [copy,777,flip.1] store(a_1034,i18,e18)=a_1035. % 2.33/2.52 ---> New Demodulator: 779 [new_demod,778] store(a_1034,i18,e18)=a_1035. % 2.33/2.52 ** KEPT (pick-wt=6): 781 [copy,780,flip.1] store(a_1035,i19,e19)=a_1036. % 2.33/2.52 ---> New Demodulator: 782 [new_demod,781] store(a_1035,i19,e19)=a_1036. % 2.33/2.52 ** KEPT (pick-wt=6): 784 [copy,783,flip.1] store(a_1036,i20,e20)=a_1037. % 2.33/2.52 ---> New Demodulator: 785 [new_demod,784] store(a_1036,i20,e20)=a_1037. % 2.33/2.52 ** KEPT (pick-wt=6): 787 [copy,786,flip.1] store(a_1037,i21,e21)=a_1038. % 2.33/2.52 ---> New Demodulator: 788 [new_demod,787] store(a_1037,i21,e21)=a_1038. % 2.33/2.52 ** KEPT (pick-wt=6): 790 [copy,789,flip.1] store(a_1038,i22,e22)=a_1039. % 2.33/2.52 ---> New Demodulator: 791 [new_demod,790] store(a_1038,i22,e22)=a_1039. % 2.33/2.52 ** KEPT (pick-wt=6): 793 [copy,792,flip.1] store(a_1039,i23,e23)=a_1040. % 2.33/2.52 ---> New Demodulator: 794 [new_demod,793] store(a_1039,i23,e23)=a_1040. % 2.33/2.52 ** KEPT (pick-wt=6): 796 [copy,795,flip.1] store(a_1040,i24,e24)=a_1041. % 2.33/2.52 ---> New Demodulator: 797 [new_demod,796] store(a_1040,i24,e24)=a_1041. % 2.33/2.52 ** KEPT (pick-wt=6): 799 [copy,798,flip.1] store(a_1041,i25,e25)=a_1042. % 2.33/2.52 ---> New Demodulator: 800 [new_demod,799] store(a_1041,i25,e25)=a_1042. % 2.33/2.52 ** KEPT (pick-wt=6): 802 [copy,801,flip.1] store(a_1042,i26,e26)=a_1043. % 2.33/2.52 ---> New Demodulator: 803 [new_demod,802] store(a_1042,i26,e26)=a_1043. % 2.33/2.52 ** KEPT (pick-wt=6): 805 [copy,804,flip.1] store(a_1043,i27,e27)=a_1044. % 2.33/2.52 ---> New Demodulator: 806 [new_demod,805] store(a_1043,i27,e27)=a_1044. % 2.33/2.52 ** KEPT (pick-wt=6): 808 [copy,807,flip.1] store(a_1044,i28,e28)=a_1045. % 2.33/2.52 ---> New Demodulator: 809 [new_demod,808] store(a_1044,i28,e28)=a_1045. % 2.33/2.52 ** KEPT (pick-wt=6): 811 [copy,810,flip.1] store(a_1045,i29,e29)=a_1046. % 2.33/2.52 ---> New Demodulator: 812 [new_demod,811] store(a_1045,i29,e29)=a_1046. % 2.33/2.52 ** KEPT (pick-wt=6): 814 [copy,813,flip.1] store(a_1046,i30,e30)=a_1047. % 2.33/2.52 ---> New Demodulator: 815 [new_demod,814] store(a_1046,i30,e30)=a_1047. % 2.33/2.52 ** KEPT (pick-wt=6): 817 [copy,816,flip.1] store(a1,i13,e13)=a_1048. % 2.33/2.52 ---> New Demodulator: 818 [new_demod,817] store(a1,i13,e13)=a_1048. % 2.33/2.52 ** KEPT (pick-wt=6): 820 [copy,819,flip.1] store(a_1048,i1,e1)=a_1049. % 2.33/2.52 ---> New Demodulator: 821 [new_demod,820] store(a_1048,i1,e1)=a_1049. % 2.33/2.52 ** KEPT (pick-wt=6): 823 [copy,822,flip.1] store(a_1049,i19,e19)=a_1050. % 2.33/2.52 ---> New Demodulator: 824 [new_demod,823] store(a_1049,i19,e19)=a_1050. % 2.33/2.52 ** KEPT (pick-wt=6): 826 [copy,825,flip.1] store(a_1050,i4,e4)=a_1051. % 2.33/2.52 ---> New Demodulator: 827 [new_demod,826] store(a_1050,i4,e4)=a_1051. % 2.33/2.52 ** KEPT (pick-wt=6): 829 [copy,828,flip.1] store(a_1051,i9,e9)=a_1052. % 2.33/2.52 ---> New Demodulator: 830 [new_demod,829] store(a_1051,i9,e9)=a_1052. % 2.33/2.52 ** KEPT (pick-wt=6): 832 [copy,831,flip.1] store(a_1052,i30,e30)=a_1053. % 2.33/2.52 ---> New Demodulator: 833 [new_demod,832] store(a_1052,i30,e30)=a_1053. % 2.33/2.52 ** KEPT (pick-wt=6): 835 [copy,834,flip.1] store(a_1053,i2,e2)=a_1054. % 2.33/2.52 ---> New Demodulator: 836 [new_demod,835] store(a_1053,i2,e2)=a_1054. % 2.33/2.52 ** KEPT (pick-wt=6): 838 [copy,837,flip.1] store(a_1054,i15,e15)=a_1055. % 2.33/2.52 ---> New Demodulator: 839 [new_demod,838] store(a_1054,i15,e15)=a_1055. % 2.33/2.52 ** KEPT (pick-wt=6): 841 [copy,840,flip.1] store(a_1055,i25,e25)=a_1056. % 2.33/2.52 ---> New Demodulator: 842 [new_demod,841] store(a_1055,i25,e25)=a_1056. % 2.33/2.52 ** KEPT (pick-wt=6): 844 [copy,843,flip.1] store(a_1056,i18,e18)=a_1057. % 2.33/2.52 ---> New Demodulator: 845 [new_demod,844] store(a_1056,i18,e18)=a_1057. % 2.33/2.52 ** KEPT (pick-wt=6): 847 [copy,846,flip.1] store(a_1057,i20,e20)=a_1058. % 2.33/2.52 ---> New Demodulator: 848 [new_demod,847] store(a_1057,i20,e20)=a_1058. % 2.33/2.52 ** KEPT (pick-wt=6): 850 [copy,849,flip.1] store(a_1058,i8,e8)=a_1059. % 2.33/2.52 ---> New Demodulator: 851 [new_demod,850] store(a_1058,i8,e8)=a_1059. % 2.33/2.52 ** KEPT (pick-wt=6): 853 [copy,852,flip.1] store(a_1059,i21,e21)=a_1060. % 2.33/2.52 ---> New Demodulator: 854 [new_demod,853] store(a_1059,i21,e21)=a_1060. % 2.33/2.52 ** KEPT (pick-wt=6): 856 [copy,855,flip.1] store(a_1060,i6,e6)=a_1061. % 2.33/2.52 ---> New Demodulator: 857 [new_demod,856] store(a_1060,i6,e6)=a_1061. % 2.33/2.52 ** KEPT (pick-wt=6): 859 [copy,858,flip.1] store(a_1061,i11,e11)=a_1062. % 2.33/2.52 ---> New Demodulator: 860 [new_demod,859] store(a_1061,i11,e11)=a_1062. % 2.33/2.52 ** KEPT (pick-wt=6): 862 [copy,861,flip.1] store(a_1062,i14,e14)=a_1063. % 2.33/2.52 ---> New Demodulator: 863 [new_demod,862] store(a_1062,i14,e14)=a_1063. % 2.33/2.52 ** KEPT (pick-wt=6): 865 [copy,864,flip.1] store(a_1063,i29,e29)=a_1064. % 2.33/2.52 ---> New Demodulator: 866 [new_demod,865] store(a_1063,i29,e29)=a_1064. % 2.33/2.52 ** KEPT (pick-wt=6): 868 [copy,867,flip.1] store(a_1064,i5,e5)=a_1065. % 2.33/2.52 ---> New Demodulator: 869 [new_demod,868] store(a_1064,i5,e5)=a_1065. % 2.33/2.52 ** KEPT (pick-wt=6): 871 [copy,870,flip.1] store(a_1065,i26,e26)=a_1066. % 2.33/2.52 ---> New Demodulator: 872 [new_demod,871] store(a_1065,i26,e26)=a_1066. % 2.33/2.52 ** KEPT (pick-wt=6): 874 [copy,873,flip.1] store(a_1066,i22,e22)=a_1067. % 2.33/2.52 ---> New Demodulator: 875 [new_demod,874] store(a_1066,i22,e22)=a_1067. % 2.33/2.52 ** KEPT (pick-wt=6): 877 [copy,876,flip.1] store(a_1067,i27,e27)=a_1068. % 2.33/2.52 ---> New Demodulator: 878 [new_demod,877] store(a_1067,i27,e27)=a_1068. % 2.33/2.52 ** KEPT (pick-wt=6): 880 [copy,879,flip.1] store(a_1068,i3,e3)=a_1069. % 2.33/2.52 ---> New Demodulator: 881 [new_demod,880] store(a_1068,i3,e3)=a_1069. % 2.33/2.52 ** KEPT (pick-wt=6): 883 [copy,882,flip.1] store(a_1069,i12,e12)=a_1070. % 2.33/2.52 ---> New Demodulator: 884 [new_demod,883] store(a_1069,i12,e12)=a_1070. % 2.33/2.52 ** KEPT (pick-wt=6): 886 [copy,885,flip.1] store(a_1070,i16,e16)=a_1071. % 2.33/2.52 ---> New Demodulator: 887 [new_demod,886] store(a_1070,i16,e16)=a_1071. % 2.33/2.52 ** KEPT (pick-wt=6): 889 [copy,888,flip.1] store(a_1071,i28,e28)=a_1072. % 2.33/2.52 ---> New Demodulator: 890 [new_demod,889] store(a_1071,i28,e28)=a_1072. % 2.33/2.52 ** KEPT (pick-wt=6): 892 [copy,891,flip.1] store(a_1072,i17,e17)=a_1073. % 2.33/2.52 ---> New Demodulator: 893 [new_demod,892] store(a_1072,i17,e17)=a_1073. % 2.33/2.52 ** KEPT (pick-wt=6): 895 [copy,894,flip.1] store(a_1073,i23,e23)=a_1074. % 2.33/2.52 ---> New Demodulator: 896 [new_demod,895] store(a_1073,i23,e23)=a_1074. % 2.33/2.52 ** KEPT (pick-wt=6): 898 [copy,897,flip.1] store(a_1074,i24,e24)=a_1075. % 2.33/2.52 ---> New Demodulator: 899 [new_demod,898] store(a_1074,i24,e24)=a_1075. % 2.33/2.52 ** KEPT (pick-wt=6): 901 [copy,900,flip.1] store(a_1075,i7,e7)=a_1076. % 2.33/2.52 ---> New Demodulator: 902 [new_demod,901] store(a_1075,i7,e7)=a_1076. % 2.33/2.52 ** KEPT (pick-wt=6): 904 [copy,903,flip.1] store(a_1076,i10,e10)=a_1077. % 2.33/2.52 ---> New Demodulator: 905 [new_demod,904] store(a_1076,i10,e10)=a_1077. % 2.33/2.52 Following clause subsumed by 717 during input processing: 0 [copy,717,flip.1] A=A. % 2.33/2.52 >>>> Starting back demodulation with 719. % 2.33/2.52 >>>> Starting back demodulation with 722. % 2.33/2.52 >>>> Starting back demodulation with 724. % 2.33/2.52 >>>> Starting back demodulation with 728. % 2.33/2.52 >>>> Starting back demodulation with 731. % 2.33/2.52 >>>> Starting back demodulation with 734. % 2.33/2.52 >>>> Starting back demodulation with 737. % 2.33/2.52 >>>> Starting back demodulation with 740. % 2.33/2.52 >>>> Starting back demodulation with 743. % 2.33/2.52 >>>> Starting back demodulation with 746. % 2.33/2.52 >>>> Starting back demodulation with 749. % 2.33/2.52 >>>> Starting back demodulation with 752. % 2.33/2.52 >>>> Starting back demodulation with 755. % 2.33/2.52 >>>> Starting back demodulation with 758. % 2.33/2.52 >>>> Starting back demodulation with 761. % 2.33/2.52 >>>> Starting back demodulation with 764. % 2.33/2.52 >>>> Starting back demodulation with 767. % 2.33/2.52 >>>> Starting back demodulation with 770. % 2.33/2.52 >>>> Starting back demodulation with 773. % 2.33/2.52 >>>> Starting back demodulation with 776. % 2.33/2.52 >>>> Starting back demodulation with 779. % 2.33/2.52 >>>> Starting back demodulation with 782. % 2.33/2.52 >>>> Starting back demodulation with 785. % 2.33/2.52 >>>> Starting back demodulation with 788. % 2.33/2.52 >>>> Starting back demodulation with 791. % 2.33/2.52 >>>> Starting back demodulation with 794. % 2.33/2.52 >>>> Starting back demodulation with 797. % 2.33/2.52 >>>> Starting back demodulation with 800. % 2.33/2.52 >>>> Starting back demodulation with 803. % 2.33/2.52 >>>> Starting back demodulation with 806. % 14.61/14.80 >>>> Starting back demodulation with 809. % 14.61/14.80 >>>> Starting back demodulation with 812. % 14.61/14.80 >>>> Starting back demodulation with 815. % 14.61/14.80 >>>> Starting back demodulation with 818. % 14.61/14.80 >>>> Starting back demodulation with 821. % 14.61/14.80 >>>> Starting back demodulation with 824. % 14.61/14.80 >>>> Starting back demodulation with 827. % 14.61/14.80 >>>> Starting back demodulation with 830. % 14.61/14.80 >>>> Starting back demodulation with 833. % 14.61/14.80 >>>> Starting back demodulation with 836. % 14.61/14.80 >>>> Starting back demodulation with 839. % 14.61/14.80 >>>> Starting back demodulation with 842. % 14.61/14.80 >>>> Starting back demodulation with 845. % 14.61/14.80 >>>> Starting back demodulation with 848. % 14.61/14.80 >>>> Starting back demodulation with 851. % 14.61/14.80 >>>> Starting back demodulation with 854. % 14.61/14.80 >>>> Starting back demodulation with 857. % 14.61/14.80 >>>> Starting back demodulation with 860. % 14.61/14.80 >>>> Starting back demodulation with 863. % 14.61/14.80 >>>> Starting back demodulation with 866. % 14.61/14.80 >>>> Starting back demodulation with 869. % 14.61/14.80 >>>> Starting back demodulation with 872. % 14.61/14.80 >>>> Starting back demodulation with 875. % 14.61/14.80 >>>> Starting back demodulation with 878. % 14.61/14.80 >>>> Starting back demodulation with 881. % 14.61/14.80 >>>> Starting back demodulation with 884. % 14.61/14.80 >>>> Starting back demodulation with 887. % 14.61/14.80 >>>> Starting back demodulation with 890. % 14.61/14.80 >>>> Starting back demodulation with 893. % 14.61/14.80 >>>> Starting back demodulation with 896. % 14.61/14.80 >>>> Starting back demodulation with 899. % 14.61/14.80 >>>> Starting back demodulation with 902. % 14.61/14.80 >>>> Starting back demodulation with 905. % 14.61/14.80 % 14.61/14.80 ======= end of input processing ======= % 14.61/14.80 % 14.61/14.80 =========== start of search =========== % 14.61/14.80 % 14.61/14.80 % 14.61/14.80 Resetting weight limit to 10. % 14.61/14.80 % 14.61/14.80 % 14.61/14.80 Resetting weight limit to 10. % 14.61/14.80 % 14.61/14.80 sos_size=2385 % 14.61/14.80 % 14.61/14.80 % 14.61/14.80 Resetting weight limit to 9. % 14.61/14.80 % 14.61/14.80 % 14.61/14.80 Resetting weight limit to 9. % 14.61/14.80 % 14.61/14.80 sos_size=2260 % 14.61/14.80 % 14.61/14.80 % 14.61/14.80 Resetting weight limit to 8. % 14.61/14.80 % 14.61/14.80 % 14.61/14.80 Resetting weight limit to 8. % 14.61/14.80 % 14.61/14.80 sos_size=2266 % 14.61/14.80 % 14.61/14.80 Search stopped because sos empty. % 14.61/14.80 % 14.61/14.80 % 14.61/14.80 Search stopped because sos empty. % 14.61/14.80 % 14.61/14.80 ============ end of search ============ % 14.61/14.80 % 14.61/14.80 -------------- statistics ------------- % 14.61/14.80 clauses given 7974 % 14.61/14.80 clauses generated 2512827 % 14.61/14.80 clauses kept 9754 % 14.61/14.80 clauses forward subsumed 86455 % 14.61/14.80 clauses back subsumed 29 % 14.61/14.80 Kbytes malloced 11718 % 14.61/14.80 % 14.61/14.80 ----------- times (seconds) ----------- % 14.61/14.80 user CPU time 12.27 (0 hr, 0 min, 12 sec) % 14.61/14.80 system CPU time 0.02 (0 hr, 0 min, 0 sec) % 14.61/14.80 wall-clock time 15 (0 hr, 0 min, 15 sec) % 14.61/14.80 % 14.61/14.80 Process 9410 finished Wed Jul 27 05:52:50 2022 % 14.61/14.80 Otter interrupted % 14.61/14.80 PROOF NOT FOUND %------------------------------------------------------------------------------