%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWV482+1 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n025.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:52 EDT 2022 % Result : Unknown 63.71s 63.87s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : SWV482+1 : TPTP v8.1.0. Released v4.0.0. % 0.06/0.12 % Command : otter-tptp-script %s % 0.13/0.33 % Computer : n025.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Wed Jul 27 05:44:45 EDT 2022 % 0.13/0.33 % CPUTime : % 2.73/2.89 ----- Otter 3.3f, August 2004 ----- % 2.73/2.89 The process was started by sandbox on n025.cluster.edu, % 2.73/2.89 Wed Jul 27 05:44:45 2022 % 2.73/2.89 The command was "./otter". The process ID is 11918. % 2.73/2.89 % 2.73/2.89 set(prolog_style_variables). % 2.73/2.89 set(auto). % 2.73/2.89 dependent: set(auto1). % 2.73/2.89 dependent: set(process_input). % 2.73/2.89 dependent: clear(print_kept). % 2.73/2.89 dependent: clear(print_new_demod). % 2.73/2.89 dependent: clear(print_back_demod). % 2.73/2.89 dependent: clear(print_back_sub). % 2.73/2.89 dependent: set(control_memory). % 2.73/2.89 dependent: assign(max_mem, 12000). % 2.73/2.89 dependent: assign(pick_given_ratio, 4). % 2.73/2.89 dependent: assign(stats_level, 1). % 2.73/2.89 dependent: assign(max_seconds, 10800). % 2.73/2.89 clear(print_given). % 2.73/2.89 % 2.73/2.89 formula_list(usable). % 2.73/2.89 all A (A=A). % 2.73/2.89 all X0 X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 X18 X19 X20 p(state(h(n1,n0,n0,n0,n0,n0,n1),h(n1,n0,n0,n0,n0,n0,n0)),iknows(atoms(n0,n0),enc(n0,n0,n0,n0))). % 2.73/2.89 all X0 X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 X18 X19 X20 (p(state(h(n1,n1,X1,X2,X3,X4,n1),X6),iknows(X7,enc(n0,X9,X10,X11)))->p(state(h(n1,n1,X1,X2,X3,X4,n1),X6),iknows(X7,enc(n1,X9,X10,X11)))). % 2.73/2.89 all X0 X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 X18 X19 X20 (p(state(h(n1,n1,X1,X2,X3,X4,X5),h(n1,X6,X7,X8,X9,X10,n1)),iknows(X12,enc(X13,X14,n0,X16)))->p(state(h(n1,n1,X1,X2,X3,X4,X5),h(n1,X6,X7,X8,X9,X10,n1)),iknows(X12,enc(X13,X14,n1,X16)))). % 2.73/2.89 all X0 X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 X18 X19 X20 (p(state(h(n1,X0,X1,X2,X3,X4,n1),h(n1,n1,X7,X8,X9,X10,X11)),iknows(X12,enc(X13,n0,X15,X16)))->p(state(h(n1,X0,X1,X2,X3,X4,n1),h(n1,n1,X7,X8,X9,X10,X11)),iknows(X12,enc(X13,n1,X15,X16)))). % 2.73/2.89 all X0 X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 X18 X19 X20 (p(state(X0,h(n1,n1,X2,X3,X4,X5,n1)),iknows(X7,enc(X8,X9,X10,n0)))->p(state(X0,h(n1,n1,X2,X3,X4,X5,n1)),iknows(X7,enc(X8,X9,X10,n1)))). % 2.73/2.89 all X0 X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 X18 X19 X20 (p(state(h(n1,X0,n1,X2,X3,X4,X5),X6),iknows(X7,enc(n1,X9,X10,X11)))->p(state(h(n1,X0,n1,X2,X3,X4,n1),X6),iknows(X7,enc(n1,X9,X10,X11)))). % 2.73/2.89 all X0 X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 X18 X19 X20 (p(state(h(n1,X0,n1,X2,X3,X4,X5),h(n0,X6,X7,X8,X9,X10,X11)),iknows(X12,enc(X13,X14,n1,X16)))->p(state(h(n1,X0,n1,X2,X3,X4,X5),h(n1,X6,X7,X8,X9,X10,n1)),iknows(X12,enc(X13,X14,n1,X16)))). % 2.73/2.89 all X0 X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 X18 X19 X20 (p(state(h(n0,X0,X1,X2,X3,X4,X5),h(n1,X6,n1,X8,X9,X10,X11)),iknows(X12,enc(X13,n1,X15,X16)))->p(state(h(n1,X0,X1,X2,X3,X4,n1),h(n1,X6,n1,X8,X9,X10,X11)),iknows(X12,enc(X13,n1,X15,X16)))). % 2.73/2.89 all X0 X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 X18 X19 X20 (p(state(X0,h(n1,X1,n1,X3,X4,X5,X6)),iknows(X7,enc(X8,X9,X10,n1)))->p(state(X0,h(n1,X1,n1,X3,X4,X5,n1)),iknows(X7,enc(X8,X9,X10,n1)))). % 2.73/2.89 all X0 X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 X18 X19 X20 (p(state(h(n1,n0,n0,X2,n0,X4,X5),X6),X7)->p(state(h(n1,n1,n0,X2,n0,X4,X5),X6),X7)). % 2.73/2.89 all X0 X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 X18 X19 X20 (p(state(h(n1,n0,n0,n0,X3,X4,X5),X6),X7)->p(state(h(n1,n0,n1,n0,X3,X4,X5),X6),X7)). % 2.73/2.89 all X0 X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 X18 X19 X20 (p(state(h(n1,n0,n0,n0,X3,X4,X5),X6),X7)->p(state(h(n1,n0,n0,n1,X3,X4,X5),X6),X7)). % 2.73/2.89 all X0 X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 X18 X19 X20 (p(state(h(n1,n0,X1,X2,n0,X4,X5),X6),X7)->p(state(h(n1,n0,X1,X2,n1,X4,X5),X6),X7)). % 2.73/2.89 all X0 X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 X18 X19 X20 (p(state(h(n1,X0,X1,X2,X3,n0,X5),X6),X7)->p(state(h(n1,X0,X1,X2,X3,n1,X5),X6),X7)). % 2.73/2.89 all X0 X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 X18 X19 X20 (p(state(X0,h(n1,n0,n0,X3,n0,X5,X6)),X7)->p(state(X0,h(n1,n1,n0,X3,n0,X5,X6)),X7)). % 2.73/2.89 all X0 X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 X18 X19 X20 (p(state(X0,h(n1,n0,n0,n0,X4,X5,X6)),X7)->p(state(X0,h(n1,n0,n1,n0,X4,X5,X6)),X7)). % 2.73/2.89 all X0 X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 X18 X19 X20 (p(state(X0,h(n1,n0,n0,n0,X4,X5,X6)),X7)->p(state(X0,h(n1,n0,n0,n1,X4,X5,X6)),X7)). % 2.73/2.89 all X0 X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 X18 X19 X20 (p(state(X0,h(n1,n0,X2,X3,n0,X5,X6)),X7)->p(state(X0,h(n1,n0,X2,X3,n1,X5,X6)),X7)). % 2.76/2.89 all X0 X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 X18 X19 X20 (p(state(X0,h(n1,X1,X2,X3,X4,n0,X6)),X7)->p(state(X0,h(n1,X1,X2,X3,X4,n1,X6)),X7)). % 2.76/2.89 all X0 X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 X18 X19 X20 (p(state(h(n1,X0,X1,X2,X3,X4,n1),X6),X7)->p(state(h(n1,X0,X1,X2,X3,X4,n0),X6),X7)). % 2.76/2.89 all X0 X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 X18 X19 X20 (p(state(X0,h(n1,X1,X2,X3,X4,X5,n1)),X7)->p(state(X0,h(n1,X1,X2,X3,X4,X5,n0)),X7)). % 2.76/2.89 all X0 X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 X18 X19 X20 (p(state(h(n1,X0,X1,X2,n1,X4,X5),X6),iknows(atoms(n0,X8),enc(n1,X10,X11,X12)))->p(state(h(n1,X0,X1,X2,n1,X4,X5),X6),iknows(atoms(n1,X8),enc(n1,X10,X11,X12)))). % 2.76/2.89 all X0 X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 X18 X19 X20 (p(state(h(n1,X0,X1,X2,n1,X4,X5),X6),iknows(atoms(X7,n0),enc(X9,X10,n1,X12)))->p(state(h(n1,X0,X1,X2,n1,X4,X5),X6),iknows(atoms(X7,n1),enc(X9,X10,n1,X12)))). % 2.76/2.89 all X0 X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 X18 X19 X20 (p(state(X0,h(n1,X1,X2,X3,n1,X5,X6)),iknows(atoms(n0,X8),enc(X9,n1,X11,X12)))->p(state(X0,h(n1,X1,X2,X3,n1,X5,X6)),iknows(atoms(n1,X8),enc(X9,n1,X11,X12)))). % 2.76/2.89 all X0 X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 X18 X19 X20 (p(state(X0,h(n1,X1,X2,X3,n1,X5,X6)),iknows(atoms(X7,n0),enc(X9,X10,X11,n1)))->p(state(X0,h(n1,X1,X2,X3,n1,X5,X6)),iknows(atoms(X7,n1),enc(X9,X10,X11,n1)))). % 2.76/2.89 all X0 X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 X18 X19 X20 (p(state(h(n1,X0,X1,n1,X3,X4,X5),X6),iknows(atoms(n1,X8),enc(n0,X10,X11,X12)))->p(state(h(n1,X0,X1,n1,X3,X4,X5),X6),iknows(atoms(n1,X8),enc(n1,X10,X11,X12)))). % 2.76/2.89 all X0 X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 X18 X19 X20 (p(state(h(n1,X0,X1,n1,X3,X4,X5),X6),iknows(atoms(X7,n1),enc(X9,X10,n0,X12)))->p(state(h(n1,X0,X1,n1,X3,X4,X5),X6),iknows(atoms(X7,n1),enc(X9,X10,n1,X12)))). % 2.76/2.89 all X0 X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 X18 X19 X20 (p(state(X0,h(n1,X1,X2,n1,X4,X5,X6)),iknows(atoms(n1,X8),enc(X9,n0,X11,X12)))->p(state(X0,h(n1,X1,X2,n1,X4,X5,X6)),iknows(atoms(n1,X8),enc(X9,n1,X11,X12)))). % 2.76/2.89 all X0 X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 X18 X19 X20 (p(state(X0,h(n1,X1,X2,n1,X4,X5,X6)),iknows(atoms(X7,n1),enc(X9,X10,X11,n0)))->p(state(X0,h(n1,X1,X2,n1,X4,X5,X6)),iknows(atoms(X7,n1),enc(X9,X10,X11,n1)))). % 2.76/2.89 all X0 X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 X18 X19 X20 (p(state(X0,X1),iknows(atoms(n1,X3),enc(n0,X5,X6,X7)))->p(state(X0,X1),iknows(atoms(n1,X3),enc(n1,X5,X6,X7)))). % 2.76/2.89 all X0 X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 X18 X19 X20 (p(state(X0,X1),iknows(atoms(n1,n1),enc(X4,X5,n0,X7)))->p(state(X0,X1),iknows(atoms(n1,n1),enc(X4,X5,n1,X7)))). % 2.76/2.89 all X0 X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 X18 X19 X20 (p(state(X0,X1),iknows(atoms(n1,n1),enc(X4,n0,X6,X7)))->p(state(X0,X1),iknows(atoms(n1,n1),enc(X4,n1,X6,X7)))). % 2.76/2.89 all X0 X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 X18 X19 X20 (p(state(X0,X1),iknows(atoms(X2,n1),enc(X4,X5,X6,n0)))->p(state(X0,X1),iknows(atoms(X2,n1),enc(X4,X5,X6,n1)))). % 2.76/2.89 all X0 X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 X18 X19 X20 (p(state(X0,X1),iknows(atoms(n1,X3),enc(n1,X5,X6,X7)))->p(state(X0,X1),iknows(atoms(n1,X3),enc(n1,X5,X6,X7)))). % 2.76/2.89 all X0 X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 X18 X19 X20 (p(state(X0,X1),iknows(atoms(n1,n0),enc(X4,X5,n1,X7)))->p(state(X0,X1),iknows(atoms(X2,n1),enc(X4,X5,n1,X7)))). % 2.76/2.89 all X0 X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 X18 X19 X20 (p(state(X0,X1),iknows(atoms(n0,n1),enc(X4,n1,X6,X7)))->p(state(X0,X1),iknows(atoms(n1,X3),enc(X4,n1,X6,X7)))). % 2.76/2.89 all X0 X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 X18 X19 X20 (p(state(X0,X1),iknows(atoms(X2,n1),enc(X4,X5,X6,n1)))->p(state(X0,X1),iknows(atoms(X2,n1),enc(X4,X5,X6,n1)))). % 2.76/2.89 all X0 X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 X18 X19 X20 (p(state(h(X0,X1,X2,X3,X4,X5,X6),h(X7,X8,X9,X10,X11,X12,X13)),iknows(atoms(X14,X15),enc(X16,X17,X18,X19)))-> -(X0=n1<->X0=n0)& -(X1=n1<->X1=n0)& -(X2=n1<->X2=n0)& -(X3=n1<->X3=n0)& -(X4=n1<->X4=n0)& -(X5=n1<->X5=n0)& -(X6=n1<->X6=n0)& -(X7=n1<->X7=n0)& -(X8=n1<->X8=n0)& -(X9=n1<->X9=n0)& -(X10=n1<->X10=n0)& -(X11=n1<->X11=n0)& -(X12=n1<->X12=n0)& -(X13=n1<->X13=n0)& -(X14=n1<->X14=n0)& -(X15=n1<->X15=n0)& -(X16=n1<->X16=n0)& -(X17=n1<->X17=n0)& -(X18=n1<->X18=n0)& -(X19=n1<->X19=n0)). % 2.76/2.89 -(exists X Y X1 X2 p(X,iknows(atoms(n1,X1),Y))). % 2.76/2.89 end_of_list. % 2.76/2.89 % 2.76/2.89 -------> usable clausifies to: % 2.76/2.89 % 2.76/2.89 list(usable). % 2.76/2.89 0 [] A=A. % 2.76/2.89 0 [] p(state(h(n1,n0,n0,n0,n0,n0,n1),h(n1,n0,n0,n0,n0,n0,n0)),iknows(atoms(n0,n0),enc(n0,n0,n0,n0))). % 2.76/2.89 0 [] -p(state(h(n1,n1,X1,X2,X3,X4,n1),X6),iknows(X7,enc(n0,X9,X10,X11)))|p(state(h(n1,n1,X1,X2,X3,X4,n1),X6),iknows(X7,enc(n1,X9,X10,X11))). % 2.76/2.89 0 [] -p(state(h(n1,n1,X1,X2,X3,X4,X5),h(n1,X6,X7,X8,X9,X10,n1)),iknows(X12,enc(X13,X14,n0,X16)))|p(state(h(n1,n1,X1,X2,X3,X4,X5),h(n1,X6,X7,X8,X9,X10,n1)),iknows(X12,enc(X13,X14,n1,X16))). % 2.76/2.89 0 [] -p(state(h(n1,X0,X1,X2,X3,X4,n1),h(n1,n1,X7,X8,X9,X10,X11)),iknows(X12,enc(X13,n0,X15,X16)))|p(state(h(n1,X0,X1,X2,X3,X4,n1),h(n1,n1,X7,X8,X9,X10,X11)),iknows(X12,enc(X13,n1,X15,X16))). % 2.76/2.89 0 [] -p(state(X0,h(n1,n1,X2,X3,X4,X5,n1)),iknows(X7,enc(X8,X9,X10,n0)))|p(state(X0,h(n1,n1,X2,X3,X4,X5,n1)),iknows(X7,enc(X8,X9,X10,n1))). % 2.76/2.89 0 [] -p(state(h(n1,X0,n1,X2,X3,X4,X5),X6),iknows(X7,enc(n1,X9,X10,X11)))|p(state(h(n1,X0,n1,X2,X3,X4,n1),X6),iknows(X7,enc(n1,X9,X10,X11))). % 2.76/2.89 0 [] -p(state(h(n1,X0,n1,X2,X3,X4,X5),h(n0,X6,X7,X8,X9,X10,X11)),iknows(X12,enc(X13,X14,n1,X16)))|p(state(h(n1,X0,n1,X2,X3,X4,X5),h(n1,X6,X7,X8,X9,X10,n1)),iknows(X12,enc(X13,X14,n1,X16))). % 2.76/2.89 0 [] -p(state(h(n0,X0,X1,X2,X3,X4,X5),h(n1,X6,n1,X8,X9,X10,X11)),iknows(X12,enc(X13,n1,X15,X16)))|p(state(h(n1,X0,X1,X2,X3,X4,n1),h(n1,X6,n1,X8,X9,X10,X11)),iknows(X12,enc(X13,n1,X15,X16))). % 2.76/2.89 0 [] -p(state(X0,h(n1,X1,n1,X3,X4,X5,X6)),iknows(X7,enc(X8,X9,X10,n1)))|p(state(X0,h(n1,X1,n1,X3,X4,X5,n1)),iknows(X7,enc(X8,X9,X10,n1))). % 2.76/2.89 0 [] -p(state(h(n1,n0,n0,X2,n0,X4,X5),X6),X7)|p(state(h(n1,n1,n0,X2,n0,X4,X5),X6),X7). % 2.76/2.89 0 [] -p(state(h(n1,n0,n0,n0,X3,X4,X5),X6),X7)|p(state(h(n1,n0,n1,n0,X3,X4,X5),X6),X7). % 2.76/2.89 0 [] -p(state(h(n1,n0,n0,n0,X3,X4,X5),X6),X7)|p(state(h(n1,n0,n0,n1,X3,X4,X5),X6),X7). % 2.76/2.89 0 [] -p(state(h(n1,n0,X1,X2,n0,X4,X5),X6),X7)|p(state(h(n1,n0,X1,X2,n1,X4,X5),X6),X7). % 2.76/2.89 0 [] -p(state(h(n1,X0,X1,X2,X3,n0,X5),X6),X7)|p(state(h(n1,X0,X1,X2,X3,n1,X5),X6),X7). % 2.76/2.89 0 [] -p(state(X0,h(n1,n0,n0,X3,n0,X5,X6)),X7)|p(state(X0,h(n1,n1,n0,X3,n0,X5,X6)),X7). % 2.76/2.89 0 [] -p(state(X0,h(n1,n0,n0,n0,X4,X5,X6)),X7)|p(state(X0,h(n1,n0,n1,n0,X4,X5,X6)),X7). % 2.76/2.89 0 [] -p(state(X0,h(n1,n0,n0,n0,X4,X5,X6)),X7)|p(state(X0,h(n1,n0,n0,n1,X4,X5,X6)),X7). % 2.76/2.89 0 [] -p(state(X0,h(n1,n0,X2,X3,n0,X5,X6)),X7)|p(state(X0,h(n1,n0,X2,X3,n1,X5,X6)),X7). % 2.76/2.89 0 [] -p(state(X0,h(n1,X1,X2,X3,X4,n0,X6)),X7)|p(state(X0,h(n1,X1,X2,X3,X4,n1,X6)),X7). % 2.76/2.89 0 [] -p(state(h(n1,X0,X1,X2,X3,X4,n1),X6),X7)|p(state(h(n1,X0,X1,X2,X3,X4,n0),X6),X7). % 2.76/2.89 0 [] -p(state(X0,h(n1,X1,X2,X3,X4,X5,n1)),X7)|p(state(X0,h(n1,X1,X2,X3,X4,X5,n0)),X7). % 2.76/2.89 0 [] -p(state(h(n1,X0,X1,X2,n1,X4,X5),X6),iknows(atoms(n0,X8),enc(n1,X10,X11,X12)))|p(state(h(n1,X0,X1,X2,n1,X4,X5),X6),iknows(atoms(n1,X8),enc(n1,X10,X11,X12))). % 2.76/2.89 0 [] -p(state(h(n1,X0,X1,X2,n1,X4,X5),X6),iknows(atoms(X7,n0),enc(X9,X10,n1,X12)))|p(state(h(n1,X0,X1,X2,n1,X4,X5),X6),iknows(atoms(X7,n1),enc(X9,X10,n1,X12))). % 2.76/2.89 0 [] -p(state(X0,h(n1,X1,X2,X3,n1,X5,X6)),iknows(atoms(n0,X8),enc(X9,n1,X11,X12)))|p(state(X0,h(n1,X1,X2,X3,n1,X5,X6)),iknows(atoms(n1,X8),enc(X9,n1,X11,X12))). % 2.76/2.89 0 [] -p(state(X0,h(n1,X1,X2,X3,n1,X5,X6)),iknows(atoms(X7,n0),enc(X9,X10,X11,n1)))|p(state(X0,h(n1,X1,X2,X3,n1,X5,X6)),iknows(atoms(X7,n1),enc(X9,X10,X11,n1))). % 2.76/2.89 0 [] -p(state(h(n1,X0,X1,n1,X3,X4,X5),X6),iknows(atoms(n1,X8),enc(n0,X10,X11,X12)))|p(state(h(n1,X0,X1,n1,X3,X4,X5),X6),iknows(atoms(n1,X8),enc(n1,X10,X11,X12))). % 2.76/2.89 0 [] -p(state(h(n1,X0,X1,n1,X3,X4,X5),X6),iknows(atoms(X7,n1),enc(X9,X10,n0,X12)))|p(state(h(n1,X0,X1,n1,X3,X4,X5),X6),iknows(atoms(X7,n1),enc(X9,X10,n1,X12))). % 2.76/2.89 0 [] -p(state(X0,h(n1,X1,X2,n1,X4,X5,X6)),iknows(atoms(n1,X8),enc(X9,n0,X11,X12)))|p(state(X0,h(n1,X1,X2,n1,X4,X5,X6)),iknows(atoms(n1,X8),enc(X9,n1,X11,X12))). % 2.76/2.90 0 [] -p(state(X0,h(n1,X1,X2,n1,X4,X5,X6)),iknows(atoms(X7,n1),enc(X9,X10,X11,n0)))|p(state(X0,h(n1,X1,X2,n1,X4,X5,X6)),iknows(atoms(X7,n1),enc(X9,X10,X11,n1))). % 2.76/2.90 0 [] -p(state(X0,X1),iknows(atoms(n1,X3),enc(n0,X5,X6,X7)))|p(state(X0,X1),iknows(atoms(n1,X3),enc(n1,X5,X6,X7))). % 2.76/2.90 0 [] -p(state(X0,X1),iknows(atoms(n1,n1),enc(X4,X5,n0,X7)))|p(state(X0,X1),iknows(atoms(n1,n1),enc(X4,X5,n1,X7))). % 2.76/2.90 0 [] -p(state(X0,X1),iknows(atoms(n1,n1),enc(X4,n0,X6,X7)))|p(state(X0,X1),iknows(atoms(n1,n1),enc(X4,n1,X6,X7))). % 2.76/2.90 0 [] -p(state(X0,X1),iknows(atoms(X2,n1),enc(X4,X5,X6,n0)))|p(state(X0,X1),iknows(atoms(X2,n1),enc(X4,X5,X6,n1))). % 2.76/2.90 0 [] -p(state(X0,X1),iknows(atoms(n1,n0),enc(X4,X5,n1,X7)))|p(state(X0,X1),iknows(atoms(X2,n1),enc(X4,X5,n1,X7))). % 2.76/2.90 0 [] -p(state(X0,X1),iknows(atoms(n0,n1),enc(X4,n1,X6,X7)))|p(state(X0,X1),iknows(atoms(n1,X3),enc(X4,n1,X6,X7))). % 2.76/2.90 0 [] -p(state(h(X0,X1,X2,X3,X4,X5,X6),h(X7,X8,X9,X10,X11,X12,X13)),iknows(atoms(X14,X15),enc(X16,X17,X18,X19)))|X0=n1|X0=n0. % 2.76/2.90 0 [] -p(state(h(X0,X1,X2,X3,X4,X5,X6),h(X7,X8,X9,X10,X11,X12,X13)),iknows(atoms(X14,X15),enc(X16,X17,X18,X19)))|X0!=n1|X0!=n0. % 2.76/2.90 0 [] -p(state(h(X0,X1,X2,X3,X4,X5,X6),h(X7,X8,X9,X10,X11,X12,X13)),iknows(atoms(X14,X15),enc(X16,X17,X18,X19)))|X1=n1|X1=n0. % 2.76/2.90 0 [] -p(state(h(X0,X1,X2,X3,X4,X5,X6),h(X7,X8,X9,X10,X11,X12,X13)),iknows(atoms(X14,X15),enc(X16,X17,X18,X19)))|X1!=n1|X1!=n0. % 2.76/2.90 0 [] -p(state(h(X0,X1,X2,X3,X4,X5,X6),h(X7,X8,X9,X10,X11,X12,X13)),iknows(atoms(X14,X15),enc(X16,X17,X18,X19)))|X2=n1|X2=n0. % 2.76/2.90 0 [] -p(state(h(X0,X1,X2,X3,X4,X5,X6),h(X7,X8,X9,X10,X11,X12,X13)),iknows(atoms(X14,X15),enc(X16,X17,X18,X19)))|X2!=n1|X2!=n0. % 2.76/2.90 0 [] -p(state(h(X0,X1,X2,X3,X4,X5,X6),h(X7,X8,X9,X10,X11,X12,X13)),iknows(atoms(X14,X15),enc(X16,X17,X18,X19)))|X3=n1|X3=n0. % 2.76/2.90 0 [] -p(state(h(X0,X1,X2,X3,X4,X5,X6),h(X7,X8,X9,X10,X11,X12,X13)),iknows(atoms(X14,X15),enc(X16,X17,X18,X19)))|X3!=n1|X3!=n0. % 2.76/2.90 0 [] -p(state(h(X0,X1,X2,X3,X4,X5,X6),h(X7,X8,X9,X10,X11,X12,X13)),iknows(atoms(X14,X15),enc(X16,X17,X18,X19)))|X4=n1|X4=n0. % 2.76/2.90 0 [] -p(state(h(X0,X1,X2,X3,X4,X5,X6),h(X7,X8,X9,X10,X11,X12,X13)),iknows(atoms(X14,X15),enc(X16,X17,X18,X19)))|X4!=n1|X4!=n0. % 2.76/2.90 0 [] -p(state(h(X0,X1,X2,X3,X4,X5,X6),h(X7,X8,X9,X10,X11,X12,X13)),iknows(atoms(X14,X15),enc(X16,X17,X18,X19)))|X5=n1|X5=n0. % 2.76/2.90 0 [] -p(state(h(X0,X1,X2,X3,X4,X5,X6),h(X7,X8,X9,X10,X11,X12,X13)),iknows(atoms(X14,X15),enc(X16,X17,X18,X19)))|X5!=n1|X5!=n0. % 2.76/2.90 0 [] -p(state(h(X0,X1,X2,X3,X4,X5,X6),h(X7,X8,X9,X10,X11,X12,X13)),iknows(atoms(X14,X15),enc(X16,X17,X18,X19)))|X6=n1|X6=n0. % 2.76/2.90 0 [] -p(state(h(X0,X1,X2,X3,X4,X5,X6),h(X7,X8,X9,X10,X11,X12,X13)),iknows(atoms(X14,X15),enc(X16,X17,X18,X19)))|X6!=n1|X6!=n0. % 2.76/2.90 0 [] -p(state(h(X0,X1,X2,X3,X4,X5,X6),h(X7,X8,X9,X10,X11,X12,X13)),iknows(atoms(X14,X15),enc(X16,X17,X18,X19)))|X7=n1|X7=n0. % 2.76/2.90 0 [] -p(state(h(X0,X1,X2,X3,X4,X5,X6),h(X7,X8,X9,X10,X11,X12,X13)),iknows(atoms(X14,X15),enc(X16,X17,X18,X19)))|X7!=n1|X7!=n0. % 2.76/2.90 0 [] -p(state(h(X0,X1,X2,X3,X4,X5,X6),h(X7,X8,X9,X10,X11,X12,X13)),iknows(atoms(X14,X15),enc(X16,X17,X18,X19)))|X8=n1|X8=n0. % 2.76/2.90 0 [] -p(state(h(X0,X1,X2,X3,X4,X5,X6),h(X7,X8,X9,X10,X11,X12,X13)),iknows(atoms(X14,X15),enc(X16,X17,X18,X19)))|X8!=n1|X8!=n0. % 2.76/2.90 0 [] -p(state(h(X0,X1,X2,X3,X4,X5,X6),h(X7,X8,X9,X10,X11,X12,X13)),iknows(atoms(X14,X15),enc(X16,X17,X18,X19)))|X9=n1|X9=n0. % 2.76/2.90 0 [] -p(state(h(X0,X1,X2,X3,X4,X5,X6),h(X7,X8,X9,X10,X11,X12,X13)),iknows(atoms(X14,X15),enc(X16,X17,X18,X19)))|X9!=n1|X9!=n0. % 2.76/2.90 0 [] -p(state(h(X0,X1,X2,X3,X4,X5,X6),h(X7,X8,X9,X10,X11,X12,X13)),iknows(atoms(X14,X15),enc(X16,X17,X18,X19)))|X10=n1|X10=n0. % 2.76/2.90 0 [] -p(state(h(X0,X1,X2,X3,X4,X5,X6),h(X7,X8,X9,X10,X11,X12,X13)),iknows(atoms(X14,X15),enc(X16,X17,X18,X19)))|X10!=n1|X10!=n0. % 2.76/2.90 0 [] -p(state(h(X0,X1,X2,X3,X4,X5,X6),h(X7,X8,X9,X10,X11,X12,X13)),iknows(atoms(X14,X15),enc(X16,X17,X18,X19)))|X11=n1|X11=n0. % 2.76/2.90 0 [] -p(state(h(X0,X1,X2,X3,X4,X5,X6),h(X7,X8,X9,X10,X11,X12,X13)),iknows(atoms(X14,X15),enc(X16,X17,X18,X19)))|X11!=n1|X11!=n0. % 2.76/2.90 0 [] -p(state(h(X0,X1,X2,X3,X4,X5,X6),h(X7,X8,X9,X10,X11,X12,X13)),iknows(atoms(X14,X15),enc(X16,X17,X18,X19)))|X12=n1|X12=n0. % 2.76/2.90 0 [] -p(state(h(X0,X1,X2,X3,X4,X5,X6),h(X7,X8,X9,X10,X11,X12,X13)),iknows(atoms(X14,X15),enc(X16,X17,X18,X19)))|X12!=n1|X12!=n0. % 2.76/2.90 0 [] -p(state(h(X0,X1,X2,X3,X4,X5,X6),h(X7,X8,X9,X10,X11,X12,X13)),iknows(atoms(X14,X15),enc(X16,X17,X18,X19)))|X13=n1|X13=n0. % 2.76/2.90 0 [] -p(state(h(X0,X1,X2,X3,X4,X5,X6),h(X7,X8,X9,X10,X11,X12,X13)),iknows(atoms(X14,X15),enc(X16,X17,X18,X19)))|X13!=n1|X13!=n0. % 2.76/2.90 0 [] -p(state(h(X0,X1,X2,X3,X4,X5,X6),h(X7,X8,X9,X10,X11,X12,X13)),iknows(atoms(X14,X15),enc(X16,X17,X18,X19)))|X14=n1|X14=n0. % 2.76/2.90 0 [] -p(state(h(X0,X1,X2,X3,X4,X5,X6),h(X7,X8,X9,X10,X11,X12,X13)),iknows(atoms(X14,X15),enc(X16,X17,X18,X19)))|X14!=n1|X14!=n0. % 2.76/2.90 0 [] -p(state(h(X0,X1,X2,X3,X4,X5,X6),h(X7,X8,X9,X10,X11,X12,X13)),iknows(atoms(X14,X15),enc(X16,X17,X18,X19)))|X15=n1|X15=n0. % 2.76/2.90 0 [] -p(state(h(X0,X1,X2,X3,X4,X5,X6),h(X7,X8,X9,X10,X11,X12,X13)),iknows(atoms(X14,X15),enc(X16,X17,X18,X19)))|X15!=n1|X15!=n0. % 2.76/2.90 0 [] -p(state(h(X0,X1,X2,X3,X4,X5,X6),h(X7,X8,X9,X10,X11,X12,X13)),iknows(atoms(X14,X15),enc(X16,X17,X18,X19)))|X16=n1|X16=n0. % 2.76/2.90 0 [] -p(state(h(X0,X1,X2,X3,X4,X5,X6),h(X7,X8,X9,X10,X11,X12,X13)),iknows(atoms(X14,X15),enc(X16,X17,X18,X19)))|X16!=n1|X16!=n0. % 2.76/2.90 0 [] -p(state(h(X0,X1,X2,X3,X4,X5,X6),h(X7,X8,X9,X10,X11,X12,X13)),iknows(atoms(X14,X15),enc(X16,X17,X18,X19)))|X17=n1|X17=n0. % 2.76/2.90 0 [] -p(state(h(X0,X1,X2,X3,X4,X5,X6),h(X7,X8,X9,X10,X11,X12,X13)),iknows(atoms(X14,X15),enc(X16,X17,X18,X19)))|X17!=n1|X17!=n0. % 2.76/2.90 0 [] -p(state(h(X0,X1,X2,X3,X4,X5,X6),h(X7,X8,X9,X10,X11,X12,X13)),iknows(atoms(X14,X15),enc(X16,X17,X18,X19)))|X18=n1|X18=n0. % 2.76/2.90 0 [] -p(state(h(X0,X1,X2,X3,X4,X5,X6),h(X7,X8,X9,X10,X11,X12,X13)),iknows(atoms(X14,X15),enc(X16,X17,X18,X19)))|X18!=n1|X18!=n0. % 2.76/2.90 0 [] -p(state(h(X0,X1,X2,X3,X4,X5,X6),h(X7,X8,X9,X10,X11,X12,X13)),iknows(atoms(X14,X15),enc(X16,X17,X18,X19)))|X19=n1|X19=n0. % 2.76/2.90 0 [] -p(state(h(X0,X1,X2,X3,X4,X5,X6),h(X7,X8,X9,X10,X11,X12,X13)),iknows(atoms(X14,X15),enc(X16,X17,X18,X19)))|X19!=n1|X19!=n0. % 2.76/2.90 0 [] -p(X,iknows(atoms(n1,X1),Y)). % 2.76/2.90 end_of_list. % 2.76/2.90 % 2.76/2.90 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=3. % 2.76/2.90 % 2.76/2.90 This ia a non-Horn set with equality. The strategy will be % 2.76/2.90 Knuth-Bendix, ordered hyper_res, factoring, and unit % 2.76/2.90 deletion, with positive clauses in sos and nonpositive % 2.76/2.90 clauses in usable. % 2.76/2.90 % 2.76/2.90 dependent: set(knuth_bendix). % 2.76/2.90 dependent: set(anl_eq). % 2.76/2.90 dependent: set(para_from). % 2.76/2.90 dependent: set(para_into). % 2.76/2.90 dependent: clear(para_from_right). % 2.76/2.90 dependent: clear(para_into_right). % 2.76/2.90 dependent: set(para_from_vars). % 2.76/2.90 dependent: set(eq_units_both_ways). % 2.76/2.90 dependent: set(dynamic_demod_all). % 2.76/2.90 dependent: set(dynamic_demod). % 2.76/2.90 dependent: set(order_eq). % 2.76/2.90 dependent: set(back_demod). % 2.76/2.90 dependent: set(lrpo). % 2.76/2.90 dependent: set(hyper_res). % 2.76/2.90 dependent: set(unit_deletion). % 2.76/2.90 dependent: set(factor). % 2.76/2.90 % 2.76/2.90 ------------> process usable: % 2.76/2.90 ** KEPT (pick-wt=36): 1 [] -p(state(h(n1,n1,A,B,C,D,n1),E),iknows(F,enc(n0,G,H,I)))|p(state(h(n1,n1,A,B,C,D,n1),E),iknows(F,enc(n1,G,H,I))). % 2.76/2.90 ** KEPT (pick-wt=50): 2 [] -p(state(h(n1,n1,A,B,C,D,E),h(n1,F,G,H,I,J,n1)),iknows(K,enc(L,M,n0,N)))|p(state(h(n1,n1,A,B,C,D,E),h(n1,F,G,H,I,J,n1)),iknows(K,enc(L,M,n1,N))). % 2.76/2.90 ** KEPT (pick-wt=50): 3 [] -p(state(h(n1,A,B,C,D,E,n1),h(n1,n1,F,G,H,I,J)),iknows(K,enc(L,n0,M,N)))|p(state(h(n1,A,B,C,D,E,n1),h(n1,n1,F,G,H,I,J)),iknows(K,enc(L,n1,M,N))). % 2.76/2.90 ** KEPT (pick-wt=36): 4 [] -p(state(A,h(n1,n1,B,C,D,E,n1)),iknows(F,enc(G,H,I,n0)))|p(state(A,h(n1,n1,B,C,D,E,n1)),iknows(F,enc(G,H,I,n1))). % 2.76/2.90 ** KEPT (pick-wt=36): 5 [] -p(state(h(n1,A,n1,B,C,D,E),F),iknows(G,enc(n1,H,I,J)))|p(state(h(n1,A,n1,B,C,D,n1),F),iknows(G,enc(n1,H,I,J))). % 2.76/2.90 ** KEPT (pick-wt=50): 6 [] -p(state(h(n1,A,n1,B,C,D,E),h(n0,F,G,H,I,J,K)),iknows(L,enc(M,N,n1,O)))|p(state(h(n1,A,n1,B,C,D,E),h(n1,F,G,H,I,J,n1)),iknows(L,enc(M,N,n1,O))). % 2.76/2.90 ** KEPT (pick-wt=50): 7 [] -p(state(h(n0,A,B,C,D,E,F),h(n1,G,n1,H,I,J,K)),iknows(L,enc(M,n1,N,O)))|p(state(h(n1,A,B,C,D,E,n1),h(n1,G,n1,H,I,J,K)),iknows(L,enc(M,n1,N,O))). % 2.76/2.90 ** KEPT (pick-wt=36): 8 [] -p(state(A,h(n1,B,n1,C,D,E,F)),iknows(G,enc(H,I,J,n1)))|p(state(A,h(n1,B,n1,C,D,E,n1)),iknows(G,enc(H,I,J,n1))). % 2.76/2.90 ** KEPT (pick-wt=24): 9 [] -p(state(h(n1,n0,n0,A,n0,B,C),D),E)|p(state(h(n1,n1,n0,A,n0,B,C),D),E). % 2.76/2.90 ** KEPT (pick-wt=24): 10 [] -p(state(h(n1,n0,n0,n0,A,B,C),D),E)|p(state(h(n1,n0,n1,n0,A,B,C),D),E). % 2.76/2.90 ** KEPT (pick-wt=24): 11 [] -p(state(h(n1,n0,n0,n0,A,B,C),D),E)|p(state(h(n1,n0,n0,n1,A,B,C),D),E). % 2.76/2.90 ** KEPT (pick-wt=24): 12 [] -p(state(h(n1,n0,A,B,n0,C,D),E),F)|p(state(h(n1,n0,A,B,n1,C,D),E),F). % 2.76/2.90 ** KEPT (pick-wt=24): 13 [] -p(state(h(n1,A,B,C,D,n0,E),F),G)|p(state(h(n1,A,B,C,D,n1,E),F),G). % 2.76/2.90 ** KEPT (pick-wt=24): 14 [] -p(state(A,h(n1,n0,n0,B,n0,C,D)),E)|p(state(A,h(n1,n1,n0,B,n0,C,D)),E). % 2.76/2.90 ** KEPT (pick-wt=24): 15 [] -p(state(A,h(n1,n0,n0,n0,B,C,D)),E)|p(state(A,h(n1,n0,n1,n0,B,C,D)),E). % 2.76/2.90 ** KEPT (pick-wt=24): 16 [] -p(state(A,h(n1,n0,n0,n0,B,C,D)),E)|p(state(A,h(n1,n0,n0,n1,B,C,D)),E). % 2.76/2.90 ** KEPT (pick-wt=24): 17 [] -p(state(A,h(n1,n0,B,C,n0,D,E)),F)|p(state(A,h(n1,n0,B,C,n1,D,E)),F). % 2.76/2.90 ** KEPT (pick-wt=24): 18 [] -p(state(A,h(n1,B,C,D,E,n0,F)),G)|p(state(A,h(n1,B,C,D,E,n1,F)),G). % 2.76/2.90 ** KEPT (pick-wt=24): 19 [] -p(state(h(n1,A,B,C,D,E,n1),F),G)|p(state(h(n1,A,B,C,D,E,n0),F),G). % 2.76/2.90 ** KEPT (pick-wt=24): 20 [] -p(state(A,h(n1,B,C,D,E,F,n1)),G)|p(state(A,h(n1,B,C,D,E,F,n0)),G). % 2.76/2.90 ** KEPT (pick-wt=40): 21 [] -p(state(h(n1,A,B,C,n1,D,E),F),iknows(atoms(n0,G),enc(n1,H,I,J)))|p(state(h(n1,A,B,C,n1,D,E),F),iknows(atoms(n1,G),enc(n1,H,I,J))). % 2.76/2.90 ** KEPT (pick-wt=40): 22 [] -p(state(h(n1,A,B,C,n1,D,E),F),iknows(atoms(G,n0),enc(H,I,n1,J)))|p(state(h(n1,A,B,C,n1,D,E),F),iknows(atoms(G,n1),enc(H,I,n1,J))). % 2.76/2.90 ** KEPT (pick-wt=40): 23 [] -p(state(A,h(n1,B,C,D,n1,E,F)),iknows(atoms(n0,G),enc(H,n1,I,J)))|p(state(A,h(n1,B,C,D,n1,E,F)),iknows(atoms(n1,G),enc(H,n1,I,J))). % 2.76/2.90 ** KEPT (pick-wt=40): 24 [] -p(state(A,h(n1,B,C,D,n1,E,F)),iknows(atoms(G,n0),enc(H,I,J,n1)))|p(state(A,h(n1,B,C,D,n1,E,F)),iknows(atoms(G,n1),enc(H,I,J,n1))). % 2.76/2.90 ** KEPT (pick-wt=40): 25 [] -p(state(h(n1,A,B,n1,C,D,E),F),iknows(atoms(n1,G),enc(n0,H,I,J)))|p(state(h(n1,A,B,n1,C,D,E),F),iknows(atoms(n1,G),enc(n1,H,I,J))). % 2.76/2.90 ** KEPT (pick-wt=40): 26 [] -p(state(h(n1,A,B,n1,C,D,E),F),iknows(atoms(G,n1),enc(H,I,n0,J)))|p(state(h(n1,A,B,n1,C,D,E),F),iknows(atoms(G,n1),enc(H,I,n1,J))). % 2.76/2.90 ** KEPT (pick-wt=40): 27 [] -p(state(A,h(n1,B,C,n1,D,E,F)),iknows(atoms(n1,G),enc(H,n0,I,J)))|p(state(A,h(n1,B,C,n1,D,E,F)),iknows(atoms(n1,G),enc(H,n1,I,J))). % 2.76/2.90 ** KEPT (pick-wt=40): 28 [] -p(state(A,h(n1,B,C,n1,D,E,F)),iknows(atoms(G,n1),enc(H,I,J,n0)))|p(state(A,h(n1,B,C,n1,D,E,F)),iknows(atoms(G,n1),enc(H,I,J,n1))). % 2.76/2.90 ** KEPT (pick-wt=26): 29 [] -p(state(A,B),iknows(atoms(n1,C),enc(n0,D,E,F)))|p(state(A,B),iknows(atoms(n1,C),enc(n1,D,E,F))). % 2.76/2.90 ** KEPT (pick-wt=26): 30 [] -p(state(A,B),iknows(atoms(n1,n1),enc(C,D,n0,E)))|p(state(A,B),iknows(atoms(n1,n1),enc(C,D,n1,E))). % 2.76/2.90 ** KEPT (pick-wt=26): 31 [] -p(state(A,B),iknows(atoms(n1,n1),enc(C,n0,D,E)))|p(state(A,B),iknows(atoms(n1,n1),enc(C,n1,D,E))). % 2.76/2.90 ** KEPT (pick-wt=26): 32 [] -p(state(A,B),iknows(atoms(C,n1),enc(D,E,F,n0)))|p(state(A,B),iknows(atoms(C,n1),enc(D,E,F,n1))). % 2.76/2.90 ** KEPT (pick-wt=26): 33 [] -p(state(A,B),iknows(atoms(n1,n0),enc(C,D,n1,E)))|p(state(A,B),iknows(atoms(F,n1),enc(C,D,n1,E))). % 2.76/2.90 ** KEPT (pick-wt=26): 34 [] -p(state(A,B),iknows(atoms(n0,n1),enc(C,n1,D,E)))|p(state(A,B),iknows(atoms(n1,F),enc(C,n1,D,E))). % 2.76/2.90 ** KEPT (pick-wt=33): 35 [] -p(state(h(A,B,C,D,E,F,G),h(H,I,J,K,L,M,N)),iknows(atoms(O,P),enc(Q,R,S,T)))|A=n1|A=n0. % 2.76/2.90 ** KEPT (pick-wt=33): 36 [] -p(state(h(A,B,C,D,E,F,G),h(H,I,J,K,L,M,N)),iknows(atoms(O,P),enc(Q,R,S,T)))|A!=n1|A!=n0. % 2.76/2.90 ** KEPT (pick-wt=33): 37 [] -p(state(h(A,B,C,D,E,F,G),h(H,I,J,K,L,M,N)),iknows(atoms(O,P),enc(Q,R,S,T)))|B=n1|B=n0. % 2.76/2.90 ** KEPT (pick-wt=33): 38 [] -p(state(h(A,B,C,D,E,F,G),h(H,I,J,K,L,M,N)),iknows(atoms(O,P),enc(Q,R,S,T)))|B!=n1|B!=n0. % 2.76/2.90 ** KEPT (pick-wt=33): 39 [] -p(state(h(A,B,C,D,E,F,G),h(H,I,J,K,L,M,N)),iknows(atoms(O,P),enc(Q,R,S,T)))|C=n1|C=n0. % 2.76/2.90 ** KEPT (pick-wt=33): 40 [] -p(state(h(A,B,C,D,E,F,G),h(H,I,J,K,L,M,N)),iknows(atoms(O,P),enc(Q,R,S,T)))|C!=n1|C!=n0. % 2.76/2.90 ** KEPT (pick-wt=33): 41 [] -p(state(h(A,B,C,D,E,F,G),h(H,I,J,K,L,M,N)),iknows(atoms(O,P),enc(Q,R,S,T)))|D=n1|D=n0. % 2.76/2.90 ** KEPT (pick-wt=33): 42 [] -p(state(h(A,B,C,D,E,F,G),h(H,I,J,K,L,M,N)),iknows(atoms(O,P),enc(Q,R,S,T)))|D!=n1|D!=n0. % 2.76/2.90 ** KEPT (pick-wt=33): 43 [] -p(state(h(A,B,C,D,E,F,G),h(H,I,J,K,L,M,N)),iknows(atoms(O,P),enc(Q,R,S,T)))|E=n1|E=n0. % 2.76/2.90 ** KEPT (pick-wt=33): 44 [] -p(state(h(A,B,C,D,E,F,G),h(H,I,J,K,L,M,N)),iknows(atoms(O,P),enc(Q,R,S,T)))|E!=n1|E!=n0. % 2.76/2.90 ** KEPT (pick-wt=33): 45 [] -p(state(h(A,B,C,D,E,F,G),h(H,I,J,K,L,M,N)),iknows(atoms(O,P),enc(Q,R,S,T)))|F=n1|F=n0. % 2.76/2.90 ** KEPT (pick-wt=33): 46 [] -p(state(h(A,B,C,D,E,F,G),h(H,I,J,K,L,M,N)),iknows(atoms(O,P),enc(Q,R,S,T)))|F!=n1|F!=n0. % 2.76/2.90 ** KEPT (pick-wt=33): 47 [] -p(state(h(A,B,C,D,E,F,G),h(H,I,J,K,L,M,N)),iknows(atoms(O,P),enc(Q,R,S,T)))|G=n1|G=n0. % 2.76/2.90 ** KEPT (pick-wt=33): 48 [] -p(state(h(A,B,C,D,E,F,G),h(H,I,J,K,L,M,N)),iknows(atoms(O,P),enc(Q,R,S,T)))|G!=n1|G!=n0. % 2.76/2.90 ** KEPT (pick-wt=33): 49 [] -p(state(h(A,B,C,D,E,F,G),h(H,I,J,K,L,M,N)),iknows(atoms(O,P),enc(Q,R,S,T)))|H=n1|H=n0. % 2.76/2.90 ** KEPT (pick-wt=33): 50 [] -p(state(h(A,B,C,D,E,F,G),h(H,I,J,K,L,M,N)),iknows(atoms(O,P),enc(Q,R,S,T)))|H!=n1|H!=n0. % 2.76/2.90 ** KEPT (pick-wt=33): 51 [] -p(state(h(A,B,C,D,E,F,G),h(H,I,J,K,L,M,N)),iknows(atoms(O,P),enc(Q,R,S,T)))|I=n1|I=n0. % 2.76/2.90 ** KEPT (pick-wt=33): 52 [] -p(state(h(A,B,C,D,E,F,G),h(H,I,J,K,L,M,N)),iknows(atoms(O,P),enc(Q,R,S,T)))|I!=n1|I!=n0. % 2.76/2.90 ** KEPT (pick-wt=33): 53 [] -p(state(h(A,B,C,D,E,F,G),h(H,I,J,K,L,M,N)),iknows(atoms(O,P),enc(Q,R,S,T)))|J=n1|J=n0. % 2.76/2.90 ** KEPT (pick-wt=33): 54 [] -p(state(h(A,B,C,D,E,F,G),h(H,I,J,K,L,M,N)),iknows(atoms(O,P),enc(Q,R,S,T)))|J!=n1|J!=n0. % 2.76/2.90 ** KEPT (pick-wt=33): 55 [] -p(state(h(A,B,C,D,E,F,G),h(H,I,J,K,L,M,N)),iknows(atoms(O,P),enc(Q,R,S,T)))|K=n1|K=n0. % 2.76/2.90 ** KEPT (pick-wt=33): 56 [] -p(state(h(A,B,C,D,E,F,G),h(H,I,J,K,L,M,N)),iknows(atoms(O,P),enc(Q,R,S,T)))|K!=n1|K!=n0. % 2.76/2.90 ** KEPT (pick-wt=33): 57 [] -p(state(h(A,B,C,D,E,F,G),h(H,I,J,K,L,M,N)),iknows(atoms(O,P),enc(Q,R,S,T)))|L=n1|L=n0. % 2.76/2.90 ** KEPT (pick-wt=33): 58 [] -p(state(h(A,B,C,D,E,F,G),h(H,I,J,K,L,M,N)),iknows(atoms(O,P),enc(Q,R,S,T)))|L!=n1|L!=n0. % 2.76/2.90 ** KEPT (pick-wt=33): 59 [] -p(state(h(A,B,C,D,E,F,G),h(H,I,J,K,L,M,N)),iknows(atoms(O,P),enc(Q,R,S,T)))|M=n1|M=n0. % 2.76/2.90 ** KEPT (pick-wt=33): 60 [] -p(state(h(A,B,C,D,E,F,G),h(H,I,J,K,L,M,N)),iknows(atoms(O,P),enc(Q,R,S,T)))|M!=n1|M!=n0. % 2.76/2.90 ** KEPT (pick-wt=33): 61 [] -p(state(h(A,B,C,D,E,F,G),h(H,I,J,K,L,M,N)),iknows(atoms(O,P),enc(Q,R,S,T)))|N=n1|N=n0. % 2.76/2.90 ** KEPT (pick-wt=33): 62 [] -p(state(h(A,B,C,D,E,F,G),h(H,I,J,K,L,M,N)),iknows(atoms(O,P),enc(Q,R,S,T)))|N!=n1|N!=n0. % 2.76/2.90 ** KEPT (pick-wt=33): 63 [] -p(state(h(A,B,C,D,E,F,G),h(H,I,J,K,L,M,N)),iknows(atoms(O,P),enc(Q,R,S,T)))|O=n1|O=n0. % 2.76/2.90 ** KEPT (pick-wt=33): 64 [] -p(state(h(A,B,C,D,E,F,G),h(H,I,J,K,L,M,N)),iknows(atoms(O,P),enc(Q,R,S,T)))|O!=n1|O!=n0. % 2.76/2.90 ** KEPT (pick-wt=33): 65 [] -p(state(h(A,B,C,D,E,F,G),h(H,I,J,K,L,M,N)),iknows(atoms(O,P),enc(Q,R,S,T)))|P=n1|P=n0. % 2.76/2.90 ** KEPT (pick-wt=33): 66 [] -p(state(h(A,B,C,D,E,F,G),h(H,I,J,K,L,M,N)),iknows(atoms(O,P),enc(Q,R,S,T)))|P!=n1|P!=n0. % 2.76/2.90 ** KEPT (pick-wt=33): 67 [] -p(state(h(A,B,C,D,E,F,G),h(H,I,J,K,L,M,N)),iknows(atoms(O,P),enc(Q,R,S,T)))|Q=n1|Q=n0. % 2.76/2.90 ** KEPT (pick-wt=33): 68 [] -p(state(h(A,B,C,D,E,F,G),h(H,I,J,K,L,M,N)),iknows(atoms(O,P),enc(Q,R,S,T)))|Q!=n1|Q!=n0. % 2.76/2.90 ** KEPT (pick-wt=33): 69 [] -p(state(h(A,B,C,D,E,F,G),h(H,I,J,K,L,M,N)),iknows(atoms(O,P),enc(Q,R,S,T)))|R=n1|R=n0. % 2.76/2.90 ** KEPT (pick-wt=33): 70 [] -p(state(h(A,B,C,D,E,F,G),h(H,I,J,K,L,M,N)),iknows(atoms(O,P),enc(Q,R,S,T)))|R!=n1|R!=n0. % 2.76/2.90 ** KEPT (pick-wt=33): 71 [] -p(state(h(A,B,C,D,E,F,G),h(H,I,J,K,L,M,N)),iknows(atoms(O,P),enc(Q,R,S,T)))|S=n1|S=n0. % 2.76/2.90 ** KEPT (pick-wt=33): 72 [] -p(state(h(A,B,C,D,E,F,G),h(H,I,J,K,L,M,N)),iknows(atoms(O,P),enc(Q,R,S,T)))|S!=n1|S!=n0. % 2.76/2.90 ** KEPT (pick-wt=33): 73 [] -p(state(h(A,B,C,D,E,F,G),h(H,I,J,K,L,M,N)),iknows(atoms(O,P),enc(Q,R,S,T)))|T=n1|T=n0. % 2.76/2.90 ** KEPT (pick-wt=33): 74 [] -p(state(h(A,B,C,D,E,F,G),h(H,I,J,K,L,M,N)),iknows(atoms(O,P),enc(Q,R,S,T)))|T!=n1|T!=n0. % 2.76/2.90 ** KEPT (pick-wt=7): 75 [] -p(A,iknows(atoms(n1,B),C)). % 2.76/2.90 29 back subsumes 25. % 2.76/2.90 32 back subsumes 28. % 2.76/2.90 75 back subsumes 33. % 2.76/2.90 75 back subsumes 31. % 2.76/2.90 75 back subsumes 30. % 2.76/2.90 75 back subsumes 29. % 2.76/2.90 75 back subsumes 27. % 2.76/2.90 % 2.76/2.90 ------------> process sos: % 2.76/2.90 ** KEPT (pick-wt=3): 76 [] A=A. % 2.76/2.90 ** KEPT (pick-wt=27): 77 [] p(state(h(n1,n0,n0,n0,n0,n0,n1),h(n1,n0,n0,n0,n0,n0,n0)),iknows(atoms(n0,n0),enc(n0,n0,n0,n0))). % 63.71/63.87 Following clause subsumed by 76 during input processing: 0 [copy,76,flip.1] A=A. % 63.71/63.87 % 63.71/63.87 ======= end of input processing ======= % 63.71/63.87 % 63.71/63.87 =========== start of search =========== % 63.71/63.87 % 63.71/63.87 % 63.71/63.87 Resetting weight limit to 59. % 63.71/63.87 % 63.71/63.87 % 63.71/63.87 Resetting weight limit to 59. % 63.71/63.87 % 63.71/63.87 sos_size=250 % 63.71/63.87 % 63.71/63.87 % 63.71/63.87 Resetting weight limit to 27. % 63.71/63.87 % 63.71/63.87 % 63.71/63.87 Resetting weight limit to 27. % 63.71/63.87 % 63.71/63.87 sos_size=1039 % 63.71/63.87 % 63.71/63.87 Search stopped because sos empty. % 63.71/63.87 % 63.71/63.87 % 63.71/63.87 Search stopped because sos empty. % 63.71/63.87 % 63.71/63.87 ============ end of search ============ % 63.71/63.87 % 63.71/63.87 -------------- statistics ------------- % 63.71/63.87 clauses given 1761 % 63.71/63.87 clauses generated 5263060 % 63.71/63.87 clauses kept 1836 % 63.71/63.87 clauses forward subsumed 33206 % 63.71/63.87 clauses back subsumed 7 % 63.71/63.87 Kbytes malloced 10742 % 63.71/63.87 % 63.71/63.87 ----------- times (seconds) ----------- % 63.71/63.87 user CPU time 60.96 (0 hr, 1 min, 0 sec) % 63.71/63.87 system CPU time 0.00 (0 hr, 0 min, 0 sec) % 63.71/63.87 wall-clock time 64 (0 hr, 1 min, 4 sec) % 63.71/63.87 % 63.71/63.87 Process 11918 finished Wed Jul 27 05:45:49 2022 % 63.71/63.87 Otter interrupted % 63.71/63.87 PROOF NOT FOUND %------------------------------------------------------------------------------