%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : ALG331-1 : TPTP v8.1.0. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n029.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:32 EDT 2022 % Result : Unknown 16.34s 16.61s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : ALG331-1 : TPTP v8.1.0. Released v4.1.0. % 0.12/0.13 % Command : otter-tptp-script %s % 0.13/0.34 % Computer : n029.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Wed Jul 27 04:00:14 EDT 2022 % 0.13/0.35 % CPUTime : % 1.80/2.02 ----- Otter 3.3f, August 2004 ----- % 1.80/2.02 The process was started by sandbox2 on n029.cluster.edu, % 1.80/2.02 Wed Jul 27 04:00:14 2022 % 1.80/2.02 The command was "./otter". The process ID is 20431. % 1.80/2.02 % 1.80/2.02 set(prolog_style_variables). % 1.80/2.02 set(auto). % 1.80/2.02 dependent: set(auto1). % 1.80/2.02 dependent: set(process_input). % 1.80/2.02 dependent: clear(print_kept). % 1.80/2.02 dependent: clear(print_new_demod). % 1.80/2.02 dependent: clear(print_back_demod). % 1.80/2.02 dependent: clear(print_back_sub). % 1.80/2.02 dependent: set(control_memory). % 1.80/2.02 dependent: assign(max_mem, 12000). % 1.80/2.02 dependent: assign(pick_given_ratio, 4). % 1.80/2.02 dependent: assign(stats_level, 1). % 1.80/2.02 dependent: assign(max_seconds, 10800). % 1.80/2.02 clear(print_given). % 1.80/2.02 % 1.80/2.02 list(usable). % 1.80/2.02 0 [] A=A. % 1.80/2.02 0 [] t(X,X,X,X)=X. % 1.80/2.02 0 [] t(X,Y,X,Z)=t(Y,X,Z,Y). % 1.80/2.02 0 [] -gr(X0,X1)| -gr(X2,X3)| -gr(X4,X5)| -gr(X6,X7)|gr(t(X0,X2,X4,X6),t(X1,X3,X5,X7)). % 1.80/2.02 0 [] gr(n0,n0). % 1.80/2.02 0 [] gr(n0,n1). % 1.80/2.02 0 [] -gr(n0,n2). % 1.80/2.02 0 [] -gr(n0,n3). % 1.80/2.02 0 [] -gr(n0,n4). % 1.80/2.02 0 [] gr(n0,n5). % 1.80/2.02 0 [] gr(n0,n6). % 1.80/2.02 0 [] gr(n0,n7). % 1.80/2.02 0 [] -gr(n1,n0). % 1.80/2.02 0 [] gr(n1,n1). % 1.80/2.02 0 [] -gr(n1,n2). % 1.80/2.02 0 [] gr(n1,n3). % 1.80/2.02 0 [] gr(n1,n4). % 1.80/2.02 0 [] gr(n1,n5). % 1.80/2.02 0 [] gr(n1,n6). % 1.80/2.02 0 [] gr(n1,n7). % 1.80/2.02 0 [] gr(n2,n0). % 1.80/2.02 0 [] -gr(n2,n1). % 1.80/2.02 0 [] gr(n2,n2). % 1.80/2.02 0 [] gr(n2,n3). % 1.80/2.02 0 [] gr(n2,n4). % 1.80/2.02 0 [] gr(n2,n5). % 1.80/2.02 0 [] gr(n2,n6). % 1.80/2.02 0 [] gr(n2,n7). % 1.80/2.02 0 [] -gr(n3,n0). % 1.80/2.02 0 [] -gr(n3,n1). % 1.80/2.02 0 [] gr(n3,n2). % 1.80/2.02 0 [] -gr(n3,n3). % 1.80/2.02 0 [] gr(n3,n4). % 1.80/2.02 0 [] gr(n3,n5). % 1.80/2.02 0 [] gr(n3,n6). % 1.80/2.02 0 [] gr(n3,n7). % 1.80/2.02 0 [] gr(n4,n0). % 1.80/2.02 0 [] gr(n4,n1). % 1.80/2.02 0 [] -gr(n4,n2). % 1.80/2.02 0 [] gr(n4,n3). % 1.80/2.02 0 [] gr(n4,n4). % 1.80/2.02 0 [] gr(n4,n5). % 1.80/2.02 0 [] gr(n4,n6). % 1.80/2.02 0 [] -gr(n4,n7). % 1.80/2.02 0 [] gr(n5,n0). % 1.80/2.02 0 [] gr(n5,n1). % 1.80/2.02 0 [] gr(n5,n2). % 1.80/2.02 0 [] gr(n5,n3). % 1.80/2.02 0 [] gr(n5,n4). % 1.80/2.02 0 [] gr(n5,n5). % 1.80/2.02 0 [] gr(n5,n6). % 1.80/2.02 0 [] gr(n5,n7). % 1.80/2.02 0 [] gr(n6,n0). % 1.80/2.02 0 [] gr(n6,n1). % 1.80/2.02 0 [] gr(n6,n2). % 1.80/2.02 0 [] gr(n6,n3). % 1.80/2.02 0 [] gr(n6,n4). % 1.80/2.02 0 [] gr(n6,n5). % 1.80/2.02 0 [] gr(n6,n6). % 1.80/2.02 0 [] gr(n6,n7). % 1.80/2.02 0 [] gr(n7,n0). % 1.80/2.02 0 [] gr(n7,n1). % 1.80/2.02 0 [] gr(n7,n2). % 1.80/2.02 0 [] gr(n7,n3). % 1.80/2.02 0 [] gr(n7,n4). % 1.80/2.02 0 [] gr(n7,n5). % 1.80/2.02 0 [] gr(n7,n6). % 1.80/2.02 0 [] gr(n7,n7). % 1.80/2.02 0 [] n0!=n1. % 1.80/2.02 0 [] n0!=n2. % 1.80/2.02 0 [] n0!=n3. % 1.80/2.02 0 [] n0!=n4. % 1.80/2.02 0 [] n0!=n5. % 1.80/2.02 0 [] n0!=n6. % 1.80/2.02 0 [] n0!=n7. % 1.80/2.02 0 [] n1!=n2. % 1.80/2.02 0 [] n1!=n3. % 1.80/2.02 0 [] n1!=n4. % 1.80/2.02 0 [] n1!=n5. % 1.80/2.02 0 [] n1!=n6. % 1.80/2.02 0 [] n1!=n7. % 1.80/2.02 0 [] n2!=n3. % 1.80/2.02 0 [] n2!=n4. % 1.80/2.02 0 [] n2!=n5. % 1.80/2.02 0 [] n2!=n6. % 1.80/2.02 0 [] n2!=n7. % 1.80/2.02 0 [] n3!=n4. % 1.80/2.02 0 [] n3!=n5. % 1.80/2.02 0 [] n3!=n6. % 1.80/2.02 0 [] n3!=n7. % 1.80/2.02 0 [] n4!=n5. % 1.80/2.02 0 [] n4!=n6. % 1.80/2.02 0 [] n4!=n7. % 1.80/2.02 0 [] n5!=n6. % 1.80/2.02 0 [] n5!=n7. % 1.80/2.02 0 [] n6!=n7. % 1.80/2.02 0 [] X=n0|X=n1|X=n2|X=n3|X=n4|X=n5|X=n6|X=n7. % 1.80/2.02 end_of_list. % 1.80/2.02 % 1.80/2.02 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=8. % 1.80/2.02 % 1.80/2.02 This ia a non-Horn set with equality. The strategy will be % 1.80/2.02 Knuth-Bendix, ordered hyper_res, factoring, and unit % 1.80/2.02 deletion, with positive clauses in sos and nonpositive % 1.80/2.02 clauses in usable. % 1.80/2.02 % 1.80/2.02 dependent: set(knuth_bendix). % 1.80/2.02 dependent: set(anl_eq). % 1.80/2.02 dependent: set(para_from). % 1.80/2.02 dependent: set(para_into). % 1.80/2.02 dependent: clear(para_from_right). % 1.80/2.02 dependent: clear(para_into_right). % 1.80/2.02 dependent: set(para_from_vars). % 1.80/2.02 dependent: set(eq_units_both_ways). % 1.80/2.02 dependent: set(dynamic_demod_all). % 1.80/2.02 dependent: set(dynamic_demod). % 1.80/2.02 dependent: set(order_eq). % 1.80/2.02 dependent: set(back_demod). % 1.80/2.02 dependent: set(lrpo). % 1.80/2.02 dependent: set(hyper_res). % 1.80/2.02 dependent: set(unit_deletion). % 1.80/2.02 dependent: set(factor). % 1.80/2.02 % 1.80/2.02 ------------> process usable: % 1.80/2.02 ** KEPT (pick-wt=23): 1 [] -gr(A,B)| -gr(C,D)| -gr(E,F)| -gr(G,H)|gr(t(A,C,E,G),t(B,D,F,H)). % 1.80/2.02 ** KEPT (pick-wt=3): 2 [] -gr(n0,n2). % 1.80/2.02 ** KEPT (pick-wt=3): 3 [] -gr(n0,n3). % 1.80/2.02 ** KEPT (pick-wt=3): 4 [] -gr(n0,n4). % 1.80/2.02 ** KEPT (pick-wt=3): 5 [] -gr(n1,n0). % 1.80/2.02 ** KEPT (pick-wt=3): 6 [] -gr(n1,n2). % 1.80/2.02 ** KEPT (pick-wt=3): 7 [] -gr(n2,n1). % 1.80/2.02 ** KEPT (pick-wt=3): 8 [] -gr(n3,n0). % 1.80/2.02 ** KEPT (pick-wt=3): 9 [] -gr(n3,n1). % 1.80/2.02 ** KEPT (pick-wt=3): 10 [] -gr(n3,n3). % 1.80/2.02 ** KEPT (pick-wt=3): 11 [] -gr(n4,n2). % 1.80/2.02 ** KEPT (pick-wt=3): 12 [] -gr(n4,n7). % 1.80/2.02 ** KEPT (pick-wt=3): 14 [copy,13,flip.1] n1!=n0. % 1.80/2.02 ** KEPT (pick-wt=3): 16 [copy,15,flip.1] n2!=n0. % 1.80/2.02 ** KEPT (pick-wt=3): 18 [copy,17,flip.1] n3!=n0. % 1.80/2.02 ** KEPT (pick-wt=3): 20 [copy,19,flip.1] n4!=n0. % 1.80/2.02 ** KEPT (pick-wt=3): 22 [copy,21,flip.1] n5!=n0. % 1.80/2.02 ** KEPT (pick-wt=3): 24 [copy,23,flip.1] n6!=n0. % 1.80/2.02 ** KEPT (pick-wt=3): 26 [copy,25,flip.1] n7!=n0. % 1.80/2.02 ** KEPT (pick-wt=3): 28 [copy,27,flip.1] n2!=n1. % 1.80/2.02 ** KEPT (pick-wt=3): 30 [copy,29,flip.1] n3!=n1. % 1.80/2.02 ** KEPT (pick-wt=3): 32 [copy,31,flip.1] n4!=n1. % 1.80/2.02 ** KEPT (pick-wt=3): 34 [copy,33,flip.1] n5!=n1. % 16.34/16.61 ** KEPT (pick-wt=3): 36 [copy,35,flip.1] n6!=n1. % 16.34/16.61 ** KEPT (pick-wt=3): 38 [copy,37,flip.1] n7!=n1. % 16.34/16.61 ** KEPT (pick-wt=3): 40 [copy,39,flip.1] n3!=n2. % 16.34/16.61 ** KEPT (pick-wt=3): 42 [copy,41,flip.1] n4!=n2. % 16.34/16.61 ** KEPT (pick-wt=3): 44 [copy,43,flip.1] n5!=n2. % 16.34/16.61 ** KEPT (pick-wt=3): 46 [copy,45,flip.1] n6!=n2. % 16.34/16.61 ** KEPT (pick-wt=3): 48 [copy,47,flip.1] n7!=n2. % 16.34/16.61 ** KEPT (pick-wt=3): 50 [copy,49,flip.1] n4!=n3. % 16.34/16.61 ** KEPT (pick-wt=3): 52 [copy,51,flip.1] n5!=n3. % 16.34/16.61 ** KEPT (pick-wt=3): 54 [copy,53,flip.1] n6!=n3. % 16.34/16.61 ** KEPT (pick-wt=3): 56 [copy,55,flip.1] n7!=n3. % 16.34/16.61 ** KEPT (pick-wt=3): 58 [copy,57,flip.1] n5!=n4. % 16.34/16.61 ** KEPT (pick-wt=3): 60 [copy,59,flip.1] n6!=n4. % 16.34/16.61 ** KEPT (pick-wt=3): 62 [copy,61,flip.1] n7!=n4. % 16.34/16.61 ** KEPT (pick-wt=3): 64 [copy,63,flip.1] n6!=n5. % 16.34/16.61 ** KEPT (pick-wt=3): 66 [copy,65,flip.1] n7!=n5. % 16.34/16.61 ** KEPT (pick-wt=3): 68 [copy,67,flip.1] n7!=n6. % 16.34/16.61 % 16.34/16.61 ------------> process sos: % 16.34/16.61 ** KEPT (pick-wt=3): 83 [] A=A. % 16.34/16.61 ** KEPT (pick-wt=7): 84 [] t(A,A,A,A)=A. % 16.34/16.61 ---> New Demodulator: 85 [new_demod,84] t(A,A,A,A)=A. % 16.34/16.61 ** KEPT (pick-wt=11): 86 [] t(A,B,A,C)=t(B,A,C,B). % 16.34/16.61 ** KEPT (pick-wt=3): 87 [] gr(n0,n0). % 16.34/16.61 ** KEPT (pick-wt=3): 88 [] gr(n0,n1). % 16.34/16.61 ** KEPT (pick-wt=3): 89 [] gr(n0,n5). % 16.34/16.61 ** KEPT (pick-wt=3): 90 [] gr(n0,n6). % 16.34/16.61 ** KEPT (pick-wt=3): 91 [] gr(n0,n7). % 16.34/16.61 ** KEPT (pick-wt=3): 92 [] gr(n1,n1). % 16.34/16.61 ** KEPT (pick-wt=3): 93 [] gr(n1,n3). % 16.34/16.61 ** KEPT (pick-wt=3): 94 [] gr(n1,n4). % 16.34/16.61 ** KEPT (pick-wt=3): 95 [] gr(n1,n5). % 16.34/16.61 ** KEPT (pick-wt=3): 96 [] gr(n1,n6). % 16.34/16.61 ** KEPT (pick-wt=3): 97 [] gr(n1,n7). % 16.34/16.61 ** KEPT (pick-wt=3): 98 [] gr(n2,n0). % 16.34/16.61 ** KEPT (pick-wt=3): 99 [] gr(n2,n2). % 16.34/16.61 ** KEPT (pick-wt=3): 100 [] gr(n2,n3). % 16.34/16.61 ** KEPT (pick-wt=3): 101 [] gr(n2,n4). % 16.34/16.61 ** KEPT (pick-wt=3): 102 [] gr(n2,n5). % 16.34/16.61 ** KEPT (pick-wt=3): 103 [] gr(n2,n6). % 16.34/16.61 ** KEPT (pick-wt=3): 104 [] gr(n2,n7). % 16.34/16.61 ** KEPT (pick-wt=3): 105 [] gr(n3,n2). % 16.34/16.61 ** KEPT (pick-wt=3): 106 [] gr(n3,n4). % 16.34/16.61 ** KEPT (pick-wt=3): 107 [] gr(n3,n5). % 16.34/16.61 ** KEPT (pick-wt=3): 108 [] gr(n3,n6). % 16.34/16.61 ** KEPT (pick-wt=3): 109 [] gr(n3,n7). % 16.34/16.61 ** KEPT (pick-wt=3): 110 [] gr(n4,n0). % 16.34/16.61 ** KEPT (pick-wt=3): 111 [] gr(n4,n1). % 16.34/16.61 ** KEPT (pick-wt=3): 112 [] gr(n4,n3). % 16.34/16.61 ** KEPT (pick-wt=3): 113 [] gr(n4,n4). % 16.34/16.61 ** KEPT (pick-wt=3): 114 [] gr(n4,n5). % 16.34/16.61 ** KEPT (pick-wt=3): 115 [] gr(n4,n6). % 16.34/16.61 ** KEPT (pick-wt=3): 116 [] gr(n5,n0). % 16.34/16.61 ** KEPT (pick-wt=3): 117 [] gr(n5,n1). % 16.34/16.61 ** KEPT (pick-wt=3): 118 [] gr(n5,n2). % 16.34/16.61 ** KEPT (pick-wt=3): 119 [] gr(n5,n3). % 16.34/16.61 ** KEPT (pick-wt=3): 120 [] gr(n5,n4). % 16.34/16.61 ** KEPT (pick-wt=3): 121 [] gr(n5,n5). % 16.34/16.61 ** KEPT (pick-wt=3): 122 [] gr(n5,n6). % 16.34/16.61 ** KEPT (pick-wt=3): 123 [] gr(n5,n7). % 16.34/16.61 ** KEPT (pick-wt=3): 124 [] gr(n6,n0). % 16.34/16.61 ** KEPT (pick-wt=3): 125 [] gr(n6,n1). % 16.34/16.61 ** KEPT (pick-wt=3): 126 [] gr(n6,n2). % 16.34/16.61 ** KEPT (pick-wt=3): 127 [] gr(n6,n3). % 16.34/16.61 ** KEPT (pick-wt=3): 128 [] gr(n6,n4). % 16.34/16.61 ** KEPT (pick-wt=3): 129 [] gr(n6,n5). % 16.34/16.61 ** KEPT (pick-wt=3): 130 [] gr(n6,n6). % 16.34/16.61 ** KEPT (pick-wt=3): 131 [] gr(n6,n7). % 16.34/16.61 ** KEPT (pick-wt=3): 132 [] gr(n7,n0). % 16.34/16.61 ** KEPT (pick-wt=3): 133 [] gr(n7,n1). % 16.34/16.61 ** KEPT (pick-wt=3): 134 [] gr(n7,n2). % 16.34/16.61 ** KEPT (pick-wt=3): 135 [] gr(n7,n3). % 16.34/16.61 ** KEPT (pick-wt=3): 136 [] gr(n7,n4). % 16.34/16.61 ** KEPT (pick-wt=3): 137 [] gr(n7,n5). % 16.34/16.61 ** KEPT (pick-wt=3): 138 [] gr(n7,n6). % 16.34/16.61 ** KEPT (pick-wt=3): 139 [] gr(n7,n7). % 16.34/16.61 ** KEPT (pick-wt=24): 140 [] A=n0|A=n1|A=n2|A=n3|A=n4|A=n5|A=n6|A=n7. % 16.34/16.61 Following clause subsumed by 83 during input processing: 0 [copy,83,flip.1] A=A. % 16.34/16.61 >>>> Starting back demodulation with 85. % 16.34/16.61 >> back demodulating 82 with 85. % 16.34/16.61 ** KEPT (pick-wt=11): 141 [copy,86,flip.1] t(A,B,C,A)=t(B,A,B,C). % 16.34/16.61 Following clause subsumed by 86 during input processing: 0 [copy,141,flip.1] t(A,B,A,C)=t(B,A,C,B). % 16.34/16.61 % 16.34/16.61 ======= end of input processing ======= % 16.34/16.61 % 16.34/16.61 =========== start of search =========== % 16.34/16.61 % 16.34/16.61 % 16.34/16.61 Resetting weight limit to 7. % 16.34/16.61 % 16.34/16.61 % 16.34/16.61 Resetting weight limit to 7. % 16.34/16.61 % 16.34/16.61 sos_size=14721 % 16.34/16.61 % 16.34/16.61 Search stopped in tp_alloc by max_mem option. % 16.34/16.61 % 16.34/16.61 Search stopped in tp_alloc by max_mem option. % 16.34/16.61 % 16.34/16.61 ============ end of search ============ % 16.34/16.61 % 16.34/16.61 -------------- statistics ------------- % 16.34/16.61 clauses given 56 % 16.34/16.61 clauses generated 8505473 % 16.34/16.61 clauses kept 46704 % 16.34/16.61 clauses forward subsumed 58124 % 16.34/16.61 clauses back subsumed 0 % 16.34/16.61 Kbytes malloced 11718 % 16.34/16.61 % 16.34/16.61 ----------- times (seconds) ----------- % 16.34/16.61 user CPU time 14.59 (0 hr, 0 min, 14 sec) % 16.34/16.61 system CPU time 0.01 (0 hr, 0 min, 0 sec) % 16.34/16.61 wall-clock time 16 (0 hr, 0 min, 16 sec) % 16.34/16.61 % 16.34/16.61 Process 20431 finished Wed Jul 27 04:00:30 2022 % 16.34/16.61 Otter interrupted % 16.34/16.61 PROOF NOT FOUND %------------------------------------------------------------------------------