%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : ALG188+1 : TPTP v8.1.0. Released v2.7.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n008.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 12:46:15 EDT 2022 % Result : Unknown 7.17s 7.33s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : ALG188+1 : TPTP v8.1.0. Released v2.7.0. % 0.06/0.13 % Command : otter-tptp-script %s % 0.12/0.34 % Computer : n008.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 03:52:38 EDT 2022 % 0.12/0.34 % CPUTime : % 7.17/7.33 ----- Otter 3.3f, August 2004 ----- % 7.17/7.33 The process was started by sandbox on n008.cluster.edu, % 7.17/7.33 Wed Jul 27 03:52:38 2022 % 7.17/7.33 The command was "./otter". The process ID is 6140. % 7.17/7.33 % 7.17/7.33 set(prolog_style_variables). % 7.17/7.33 set(auto). % 7.17/7.33 dependent: set(auto1). % 7.17/7.33 dependent: set(process_input). % 7.17/7.33 dependent: clear(print_kept). % 7.17/7.33 dependent: clear(print_new_demod). % 7.17/7.33 dependent: clear(print_back_demod). % 7.17/7.33 dependent: clear(print_back_sub). % 7.17/7.33 dependent: set(control_memory). % 7.17/7.33 dependent: assign(max_mem, 12000). % 7.17/7.33 dependent: assign(pick_given_ratio, 4). % 7.17/7.33 dependent: assign(stats_level, 1). % 7.17/7.33 dependent: assign(max_seconds, 10800). % 7.17/7.33 clear(print_given). % 7.17/7.33 % 7.17/7.33 formula_list(usable). % 7.17/7.33 all A (A=A). % 7.17/7.33 e0!=e1. % 7.17/7.33 e0!=e2. % 7.17/7.33 e0!=e3. % 7.17/7.33 e0!=e4. % 7.17/7.33 e1!=e2. % 7.17/7.33 e1!=e3. % 7.17/7.33 e1!=e4. % 7.17/7.33 e2!=e3. % 7.17/7.33 e2!=e4. % 7.17/7.33 e3!=e4. % 7.17/7.33 op(e0,e0)=e0. % 7.17/7.33 op(e0,e1)=e3. % 7.17/7.33 op(e0,e2)=e4. % 7.17/7.33 op(e0,e3)=e1. % 7.17/7.33 op(e0,e4)=e2. % 7.17/7.33 op(e1,e0)=e4. % 7.17/7.33 op(e1,e1)=e1. % 7.17/7.33 op(e1,e2)=e3. % 7.17/7.33 op(e1,e3)=e2. % 7.17/7.33 op(e1,e4)=e0. % 7.17/7.33 op(e2,e0)=e1. % 7.17/7.33 op(e2,e1)=e0. % 7.17/7.33 op(e2,e2)=e2. % 7.17/7.33 op(e2,e3)=e4. % 7.17/7.33 op(e2,e4)=e3. % 7.17/7.33 op(e3,e0)=e2. % 7.17/7.33 op(e3,e1)=e4. % 7.17/7.33 op(e3,e2)=e0. % 7.17/7.33 op(e3,e3)=e3. % 7.17/7.33 op(e3,e4)=e1. % 7.17/7.33 op(e4,e0)=e3. % 7.17/7.33 op(e4,e1)=e2. % 7.17/7.33 op(e4,e2)=e1. % 7.17/7.33 op(e4,e3)=e0. % 7.17/7.33 op(e4,e4)=e4. % 7.17/7.33 -(op(e0,op(e0,e0))=e0&op(e0,op(e0,e1))=e1&op(e0,op(e0,e2))=e2&op(e0,op(e0,e3))=e3&op(e0,op(e0,e4))=e4&op(e1,op(e1,e0))=e0&op(e1,op(e1,e1))=e1&op(e1,op(e1,e2))=e2&op(e1,op(e1,e3))=e3&op(e1,op(e1,e4))=e4&op(e2,op(e2,e0))=e0&op(e2,op(e2,e1))=e1&op(e2,op(e2,e2))=e2&op(e2,op(e2,e3))=e3&op(e2,op(e2,e4))=e4&op(e3,op(e3,e0))=e0&op(e3,op(e3,e1))=e1&op(e3,op(e3,e2))=e2&op(e3,op(e3,e3))=e3&op(e3,op(e3,e4))=e4&op(e4,op(e4,e0))=e0&op(e4,op(e4,e1))=e1&op(e4,op(e4,e2))=e2&op(e4,op(e4,e3))=e3&op(e4,op(e4,e4))=e4& (op(e0,e0)=e0|op(e0,e0)=e1|op(e0,e0)=e2|op(e0,e0)=e3|op(e0,e0)=e4)& (op(e0,e1)=e0|op(e0,e1)=e1|op(e0,e1)=e2|op(e0,e1)=e3|op(e0,e1)=e4)& (op(e0,e2)=e0|op(e0,e2)=e1|op(e0,e2)=e2|op(e0,e2)=e3|op(e0,e2)=e4)& (op(e0,e3)=e0|op(e0,e3)=e1|op(e0,e3)=e2|op(e0,e3)=e3|op(e0,e3)=e4)& (op(e0,e4)=e0|op(e0,e4)=e1|op(e0,e4)=e2|op(e0,e4)=e3|op(e0,e4)=e4)& (op(e1,e0)=e0|op(e1,e0)=e1|op(e1,e0)=e2|op(e1,e0)=e3|op(e1,e0)=e4)& (op(e1,e1)=e0|op(e1,e1)=e1|op(e1,e1)=e2|op(e1,e1)=e3|op(e1,e1)=e4)& (op(e1,e2)=e0|op(e1,e2)=e1|op(e1,e2)=e2|op(e1,e2)=e3|op(e1,e2)=e4)& (op(e1,e3)=e0|op(e1,e3)=e1|op(e1,e3)=e2|op(e1,e3)=e3|op(e1,e3)=e4)& (op(e1,e4)=e0|op(e1,e4)=e1|op(e1,e4)=e2|op(e1,e4)=e3|op(e1,e4)=e4)& (op(e2,e0)=e0|op(e2,e0)=e1|op(e2,e0)=e2|op(e2,e0)=e3|op(e2,e0)=e4)& (op(e2,e1)=e0|op(e2,e1)=e1|op(e2,e1)=e2|op(e2,e1)=e3|op(e2,e1)=e4)& (op(e2,e2)=e0|op(e2,e2)=e1|op(e2,e2)=e2|op(e2,e2)=e3|op(e2,e2)=e4)& (op(e2,e3)=e0|op(e2,e3)=e1|op(e2,e3)=e2|op(e2,e3)=e3|op(e2,e3)=e4)& (op(e2,e4)=e0|op(e2,e4)=e1|op(e2,e4)=e2|op(e2,e4)=e3|op(e2,e4)=e4)& (op(e3,e0)=e0|op(e3,e0)=e1|op(e3,e0)=e2|op(e3,e0)=e3|op(e3,e0)=e4)& (op(e3,e1)=e0|op(e3,e1)=e1|op(e3,e1)=e2|op(e3,e1)=e3|op(e3,e1)=e4)& (op(e3,e2)=e0|op(e3,e2)=e1|op(e3,e2)=e2|op(e3,e2)=e3|op(e3,e2)=e4)& (op(e3,e3)=e0|op(e3,e3)=e1|op(e3,e3)=e2|op(e3,e3)=e3|op(e3,e3)=e4)& (op(e3,e4)=e0|op(e3,e4)=e1|op(e3,e4)=e2|op(e3,e4)=e3|op(e3,e4)=e4)& (op(e4,e0)=e0|op(e4,e0)=e1|op(e4,e0)=e2|op(e4,e0)=e3|op(e4,e0)=e4)& (op(e4,e1)=e0|op(e4,e1)=e1|op(e4,e1)=e2|op(e4,e1)=e3|op(e4,e1)=e4)& (op(e4,e2)=e0|op(e4,e2)=e1|op(e4,e2)=e2|op(e4,e2)=e3|op(e4,e2)=e4)& (op(e4,e3)=e0|op(e4,e3)=e1|op(e4,e3)=e2|op(e4,e3)=e3|op(e4,e3)=e4)& (op(e4,e4)=e0|op(e4,e4)=e1|op(e4,e4)=e2|op(e4,e4)=e3|op(e4,e4)=e4)& (op(e0,e0)=e0|op(e0,e1)=e0|op(e0,e2)=e0|op(e0,e3)=e0|op(e0,e4)=e0)& (op(e0,e0)=e0|op(e1,e0)=e0|op(e2,e0)=e0|op(e3,e0)=e0|op(e4,e0)=e0)& (op(e0,e0)=e1|op(e0,e1)=e1|op(e0,e2)=e1|op(e0,e3)=e1|op(e0,e4)=e1)& (op(e0,e0)=e1|op(e1,e0)=e1|op(e2,e0)=e1|op(e3,e0)=e1|op(e4,e0)=e1)& (op(e0,e0)=e2|op(e0,e1)=e2|op(e0,e2)=e2|op(e0,e3)=e2|op(e0,e4)=e2)& (op(e0,e0)=e2|op(e1,e0)=e2|op(e2,e0)=e2|op(e3,e0)=e2|op(e4,e0)=e2)& (op(e0,e0)=e3|op(e0,e1)=e3|op(e0,e2)=e3|op(e0,e3)=e3|op(e0,e4)=e3)& (op(e0,e0)=e3|op(e1,e0)=e3|op(e2,e0)=e3|op(e3,e0)=e3|op(e4,e0)=e3)& (op(e0,e0)=e4|op(e0,e1)=e4|op(e0,e2)=e4|op(e0,e3)=e4|op(e0,e4)=e4)& (op(e0,e0)=e4|op(e1,e0)=e4|op(e2,e0)=e4|op(e3,e0)=e4|op(e4,e0)=e4)& (op(e1,e0)=e0|op(e1,e1)=e0|op(e1,e2)=e0|op(e1,e3)=e0|op(e1,e4)=e0)& (op(e0,e1)=e0|op(e1,e1)=e0|op(e2,e1)=e0|op(e3, % 7.17/7.33 Search stopped in tp_alloc by max_mem option. % 7.17/7.33 e1)=e0|op(e4,e1)=e0)& (op(e1,e0)=e1|op(e1,e1)=e1|op(e1,e2)=e1|op(e1,e3)=e1|op(e1,e4)=e1)& (op(e0,e1)=e1|op(e1,e1)=e1|op(e2,e1)=e1|op(e3,e1)=e1|op(e4,e1)=e1)& (op(e1,e0)=e2|op(e1,e1)=e2|op(e1,e2)=e2|op(e1,e3)=e2|op(e1,e4)=e2)& (op(e0,e1)=e2|op(e1,e1)=e2|op(e2,e1)=e2|op(e3,e1)=e2|op(e4,e1)=e2)& (op(e1,e0)=e3|op(e1,e1)=e3|op(e1,e2)=e3|op(e1,e3)=e3|op(e1,e4)=e3)& (op(e0,e1)=e3|op(e1,e1)=e3|op(e2,e1)=e3|op(e3,e1)=e3|op(e4,e1)=e3)& (op(e1,e0)=e4|op(e1,e1)=e4|op(e1,e2)=e4|op(e1,e3)=e4|op(e1,e4)=e4)& (op(e0,e1)=e4|op(e1,e1)=e4|op(e2,e1)=e4|op(e3,e1)=e4|op(e4,e1)=e4)& (op(e2,e0)=e0|op(e2,e1)=e0|op(e2,e2)=e0|op(e2,e3)=e0|op(e2,e4)=e0)& (op(e0,e2)=e0|op(e1,e2)=e0|op(e2,e2)=e0|op(e3,e2)=e0|op(e4,e2)=e0)& (op(e2,e0)=e1|op(e2,e1)=e1|op(e2,e2)=e1|op(e2,e3)=e1|op(e2,e4)=e1)& (op(e0,e2)=e1|op(e1,e2)=e1|op(e2,e2)=e1|op(e3,e2)=e1|op(e4,e2)=e1)& (op(e2,e0)=e2|op(e2,e1)=e2|op(e2,e2)=e2|op(e2,e3)=e2|op(e2,e4)=e2)& (op(e0,e2)=e2|op(e1,e2)=e2|op(e2,e2)=e2|op(e3,e2)=e2|op(e4,e2)=e2)& (op(e2,e0)=e3|op(e2,e1)=e3|op(e2,e2)=e3|op(e2,e3)=e3|op(e2,e4)=e3)& (op(e0,e2)=e3|op(e1,e2)=e3|op(e2,e2)=e3|op(e3,e2)=e3|op(e4,e2)=e3)& (op(e2,e0)=e4|op(e2,e1)=e4|op(e2,e2)=e4|op(e2,e3)=e4|op(e2,e4)=e4)& (op(e0,e2)=e4|op(e1,e2)=e4|op(e2,e2)=e4|op(e3,e2)=e4|op(e4,e2)=e4)& (op(e3,e0)=e0|op(e3,e1)=e0|op(e3,e2)=e0|op(e3,e3)=e0|op(e3,e4)=e0)& (op(e0,e3)=e0|op(e1,e3)=e0|op(e2,e3)=e0|op(e3,e3)=e0|op(e4,e3)=e0)& (op(e3,e0)=e1|op(e3,e1)=e1|op(e3,e2)=e1|op(e3,e3)=e1|op(e3,e4)=e1)& (op(e0,e3)=e1|op(e1,e3)=e1|op(e2,e3)=e1|op(e3,e3)=e1|op(e4,e3)=e1)& (op(e3,e0)=e2|op(e3,e1)=e2|op(e3,e2)=e2|op(e3,e3)=e2|op(e3,e4)=e2)& (op(e0,e3)=e2|op(e1,e3)=e2|op(e2,e3)=e2|op(e3,e3)=e2|op(e4,e3)=e2)& (op(e3,e0)=e3|op(e3,e1)=e3|op(e3,e2)=e3|op(e3,e3)=e3|op(e3,e4)=e3)& (op(e0,e3)=e3|op(e1,e3)=e3|op(e2,e3)=e3|op(e3,e3)=e3|op(e4,e3)=e3)& (op(e3,e0)=e4|op(e3,e1)=e4|op(e3,e2)=e4|op(e3,e3)=e4|op(e3,e4)=e4)& (op(e0,e3)=e4|op(e1,e3)=e4|op(e2,e3)=e4|op(e3,e3)=e4|op(e4,e3)=e4)& (op(e4,e0)=e0|op(e4,e1)=e0|op(e4,e2)=e0|op(e4,e3)=e0|op(e4,e4)=e0)& (op(e0,e4)=e0|op(e1,e4)=e0|op(e2,e4)=e0|op(e3,e4)=e0|op(e4,e4)=e0)& (op(e4,e0)=e1|op(e4,e1)=e1|op(e4,e2)=e1|op(e4,e3)=e1|op(e4,e4)=e1)& (op(e0,e4)=e1|op(e1,e4)=e1|op(e2,e4)=e1|op(e3,e4)=e1|op(e4,e4)=e1)& (op(e4,e0)=e2|op(e4,e1)=e2|op(e4,e2)=e2|op(e4,e3)=e2|op(e4,e4)=e2)& (op(e0,e4)=e2|op(e1,e4)=e2|op(e2,e4)=e2|op(e3,e4)=e2|op(e4,e4)=e2)& (op(e4,e0)=e3|op(e4,e1)=e3|op(e4,e2)=e3|op(e4,e3)=e3|op(e4,e4)=e3)& (op(e0,e4)=e3|op(e1,e4)=e3|op(e2,e4)=e3|op(e3,e4)=e3|op(e4,e4)=e3)& (op(e4,e0)=e4|op(e4,e1)=e4|op(e4,e2)=e4|op(e4,e3)=e4|op(e4,e4)=e4)& (op(e0,e4)=e4|op(e1,e4)=e4|op(e2,e4)=e4|op(e3,e4)=e4|op(e4,e4)=e4)&op(op(e0,e0),op(e0,e0))=e0&op(op(e1,e0),op(e0,e1))=e0&op(op(e2,e0),op(e0,e2))=e0&op(op(e3,e0),op(e0,e3))=e0&op(op(e4,e0),op(e0,e4))=e0&op(op(e0,e1),op(e1,e0))=e1&op(op(e1,e1),op(e1,e1))=e1&op(op(e2,e1),op(e1,e2))=e1&op(op(e3,e1),op(e1,e3))=e1&op(op(e4,e1),op(e1,e4))=e1&op(op(e0,e2),op(e2,e0))=e2&op(op(e1,e2),op(e2,e1))=e2&op(op(e2,e2),op(e2,e2))=e2&op(op(e3,e2),op(e2,e3))=e2&op(op(e4,e2),op(e2,e4))=e2&op(op(e0,e3),op(e3,e0))=e3&op(op(e1,e3),op(e3,e1))=e3&op(op(e2,e3),op(e3,e2))=e3&op(op(e3,e3),op(e3,e3))=e3&op(op(e4,e3),op(e3,e4))=e3&op(op(e0,e4),op(e4,e0))=e4&op(op(e1,e4),op(e4,e1))=e4&op(op(e2,e4),op(e4,e2))=e4&op(op(e3,e4),op(e4,e3))=e4&op(op(e4,e4),op(e4,e4))=e4). % 7.17/7.33 end_of_list. % 7.17/7.33 % 7.17/7.33 Search stopped in tp_alloc by max_mem option. % 7.17/7.33 % 7.17/7.33 ============ end of search ============ % 7.17/7.33 % 7.17/7.33 -------------- statistics ------------- % 7.17/7.33 clauses given 0 % 7.17/7.33 clauses generated 0 % 7.17/7.33 clauses kept 0 % 7.17/7.33 clauses forward subsumed 0 % 7.17/7.33 clauses back subsumed 0 % 7.17/7.33 Kbytes malloced 11718 % 7.17/7.33 % 7.17/7.33 ----------- times (seconds) ----------- % 7.17/7.33 user CPU time 4.53 (0 hr, 0 min, 4 sec) % 7.17/7.33 system CPU time 0.01 (0 hr, 0 min, 0 sec) % 7.17/7.33 wall-clock time 7 (0 hr, 0 min, 7 sec) % 7.17/7.33 % 7.17/7.33 Process 6140 finished Wed Jul 27 03:52:45 2022 % 7.17/7.33 Otter interrupted % 7.17/7.33 PROOF NOT FOUND %------------------------------------------------------------------------------