%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWV461+1 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n023.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:50 EDT 2022 % Result : Unknown 26.63s 26.80s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWV461+1 : TPTP v8.1.0. Released v4.0.0. % 0.03/0.13 % Command : otter-tptp-script %s % 0.12/0.33 % Computer : n023.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 06:26:48 EDT 2022 % 0.12/0.34 % CPUTime : % 2.34/2.53 ----- Otter 3.3f, August 2004 ----- % 2.34/2.53 The process was started by sandbox2 on n023.cluster.edu, % 2.34/2.53 Wed Jul 27 06:26:48 2022 % 2.34/2.53 The command was "./otter". The process ID is 12598. % 2.34/2.53 % 2.34/2.53 set(prolog_style_variables). % 2.34/2.53 set(auto). % 2.34/2.53 dependent: set(auto1). % 2.34/2.53 dependent: set(process_input). % 2.34/2.53 dependent: clear(print_kept). % 2.34/2.53 dependent: clear(print_new_demod). % 2.34/2.53 dependent: clear(print_back_demod). % 2.34/2.53 dependent: clear(print_back_sub). % 2.34/2.53 dependent: set(control_memory). % 2.34/2.53 dependent: assign(max_mem, 12000). % 2.34/2.53 dependent: assign(pick_given_ratio, 4). % 2.34/2.53 dependent: assign(stats_level, 1). % 2.34/2.53 dependent: assign(max_seconds, 10800). % 2.34/2.53 clear(print_given). % 2.34/2.53 % 2.34/2.53 formula_list(usable). % 2.34/2.53 all A (A=A). % 2.34/2.53 all Pid Pid2 (elem(m_Ack(Pid,Pid2),queue(host(Pid)))->setIn(Pid,pids)&setIn(Pid2,pids)). % 2.34/2.53 all P Q (s(host(P))=host(Q)->host(P)!=host(Q)). % 2.34/2.53 all P le_q(s(zero),host(P)). % 2.34/2.53 le_q(s(zero),nbr_proc). % 2.34/2.53 all P le_q(host(P),nbr_proc). % 2.34/2.53 elec_1!=elec_2. % 2.34/2.53 elec_1!=wait. % 2.34/2.53 elec_1!=norm. % 2.34/2.53 elec_2!=wait. % 2.34/2.53 elec_2!=norm. % 2.34/2.53 norm!=wait. % 2.34/2.53 all X Y Z (m_Ack(X,Y)!=m_Halt(Z)). % 2.34/2.53 all X Y Z (m_Ack(X,Y)!=m_Down(Z)). % 2.34/2.53 all X Y Z (m_Ack(X,Y)!=m_NotNorm(Z)). % 2.34/2.53 all X Y Z (m_Ack(X,Y)!=m_Ldr(Z)). % 2.34/2.53 all X Y Z (m_Ack(X,Y)!=m_NormQ(Z)). % 2.34/2.53 all X Y (m_NotNorm(X)!=m_Halt(Y)). % 2.34/2.53 all X Y (m_Down(X)!=m_Halt(Y)). % 2.34/2.53 all X Y (m_Down(X)!=m_Ldr(Y)). % 2.34/2.53 all X Y (m_Down(X)!=m_NotNorm(Y)). % 2.34/2.53 all X Y (m_Down(X)!=m_NormQ(Y)). % 2.34/2.53 all X Y (m_NormQ(X)!=m_Halt(Y)). % 2.34/2.53 all X Y (m_Ldr(X)!=m_Halt(Y)). % 2.34/2.53 all X Y (m_Ldr(X)!=m_NormQ(Y)). % 2.34/2.53 all X Y (m_Ldr(X)!=m_NotNorm(Y)). % 2.34/2.53 all X Y (m_NormQ(X)!=m_NotNorm(Y)). % 2.34/2.53 all X Y (X!=Y<->m_Halt(X)!=m_Halt(Y)). % 2.34/2.53 all X Y (X!=Y<->m_NormQ(X)!=m_NormQ(Y)). % 2.34/2.53 all X Y (X!=Y<->m_NotNorm(X)!=m_NotNorm(Y)). % 2.34/2.53 all X Y (X!=Y<->m_Ldr(X)!=m_Ldr(Y)). % 2.34/2.53 all X Y (X!=Y<->m_Down(X)!=m_Down(Y)). % 2.34/2.53 all X1 X2 Y1 Y2 (X1!=X2->m_Ack(X1,Y1)!=m_Ack(X2,Y2)). % 2.34/2.53 all X1 X2 Y1 Y2 (Y1!=Y2->m_Ack(X1,Y1)!=m_Ack(X2,Y2)). % 2.34/2.53 all Pid Pid2 (host(Pid)!=host(Pid2)->Pid!=Pid2). % 2.34/2.53 -setIn(nil,alive). % 2.34/2.53 all X Q (head(cons(X,Q))=X). % 2.34/2.53 all X Q (tail(cons(X,Q))=Q). % 2.34/2.53 all Y Q (last(snoc(Q,Y))=Y). % 2.34/2.53 all Y Q (init(snoc(Q,Y))=Q). % 2.34/2.53 all Q (Q=q_nil|Q=cons(head(Q),tail(Q))). % 2.34/2.53 all Q (Q=q_nil|Q=snoc(init(Q),last(Q))). % 2.34/2.53 all X Q (q_nil!=cons(X,Q)). % 2.34/2.53 all Y Q (q_nil!=snoc(Q,Y)). % 2.34/2.53 all X (cons(X,q_nil)=snoc(q_nil,X)). % 2.34/2.53 all X Y Q (snoc(cons(X,Q),Y)=cons(X,snoc(Q,Y))). % 2.34/2.53 all X (-elem(X,q_nil)). % 2.34/2.53 all X Y Q (elem(X,cons(Y,Q))<->X=Y|elem(X,Q)). % 2.34/2.53 all X Y Q (elem(X,snoc(Q,Y))<->X=Y|elem(X,Q)). % 2.34/2.53 all X (pidElem(X)<-> (exists Y (X=m_Halt(Y)|X=m_Down(Y)))). % 2.34/2.53 all X (pidMsg(m_Halt(X))=X). % 2.34/2.53 all X (pidMsg(m_Down(X))=X). % 2.34/2.53 ordered(q_nil). % 2.34/2.53 all X (ordered(cons(X,q_nil))&ordered(snoc(q_nil,X))). % 2.34/2.53 all X Q (ordered(cons(X,Q))<->ordered(Q)& (all Y (elem(Y,Q)&pidElem(X)&pidElem(Y)&host(pidMsg(Y))=host(pidMsg(X))->le_q(pidMsg(X),pidMsg(Y))))). % 2.34/2.53 all X Q (ordered(snoc(Q,X))<->ordered(Q)& (all Y (elem(Y,Q)&pidElem(X)&pidElem(Y)&host(pidMsg(Y))=host(pidMsg(X))->le_q(pidMsg(Y),pidMsg(X))))). % 2.34/2.53 all Q X Y (ordered(Q)->ordered(snoc(Q,m_Ack(X,Y)))). % 2.34/2.53 all Q X (ordered(Q)->ordered(snoc(Q,m_Ldr(X)))). % 2.34/2.53 all Q X Y (ordered(cons(m_Halt(X),Q))&host(X)=host(Y)&elem(m_Down(Y),Q)->le_q(X,Y)). % 2.34/2.53 all X (-le_q(s(X),X)). % 2.34/2.53 all X le_q(X,X). % 2.34/2.53 all X Y (le_q(X,Y)|le_q(Y,X)). % 2.34/2.53 all X Y (le_q(X,Y)&le_q(Y,X)<->X=Y). % 2.34/2.53 all X Y Z (le_q(X,Y)&le_q(Y,Z)->le_q(X,Z)). % 2.34/2.53 all X Y (le_q(X,Y)<->le_q(s(X),s(Y))). % 2.34/2.53 all X Y (le_q(X,s(Y))<->X=s(Y)|le_q(X,Y)). % 2.34/2.53 all X (-setIn(X,setEmpty)). % 2.34/2.53 -(all V W ((all X (host(W)=host(X)-> -setIn(X,alive)))& (all X Y (elem(m_Ldr(Y),queue(host(X)))-> -le_q(host(X),host(Y))))& (all X Y (elem(m_Down(Y),queue(host(X)))->host(Y)!=host(X)))& (all X Y (elem(m_Halt(Y),queue(host(X)))-> -le_q(host(X),host(Y))))& (all X Y Z (elem(m_Ack(Z,X),queue(host(Y)))-> -le_q(host(X),host(Z))))& (all X Y (Y!=X&host(Y)=host(X)-> -setIn(X,alive)| -setIn(Y,alive)))& (all X Y (setIn(Y,alive)&elem(m_Ack(Y,X),queue(host(Y)))->le_q(host(X),index(pendack,host(Y)))))& (all X Y (setIn(Y,alive)&index(status,host(Y))=elec_1-> -elem(m_Ack(Y,X),queue(host(Y)))))& (all X ((index(status,host(X))=elec_1|index(status,host(X))=elec_2)&setIn(X,alive)->index(elid,host(X))=X))& (all X Y Z (setIn(Z,alive)&elem(m_Down(Y),queue(host(Z)))&host(Y)=host(X)-> -(setIn(X,alive)&index(ldr,host(X))=host(X)&index(status,host(X))=norm)))& (all X Y Z (setIn(X,alive)&setIn(Z,alive)&host(Z)=host(Y)&index(status,host(X))=elec_2&index(status,host(Z))=elec_2-> -elem(m_Ack(X,Y),queue(host(X)))))& (all X Y (-le_q(host(X),host(Y))&setIn(X,alive)&setIn(Y,alive)&index(status,host(X))=elec_2&index(status,host(Y))=elec_2->le_q(index(pendack,host(Y)),host(X))))& (all X Y (-le_q(host(X),host(Y))&setIn(X,alive)&setIn(Y,alive)&index(status,host(X))=elec_2&index(status,host(Y))=elec_2-> -le_q(index(pendack,host(X)),index(pendack,host(Y)))))& (all X Y Z (-le_q(index(pendack,host(Z)),host(X))&setIn(Z,alive)&elem(m_Halt(Z),queue(host(Y)))&index(status,host(Z))=elec_2-> -(setIn(X,alive)&index(ldr,host(X))=host(X)&index(status,host(X))=norm)))& (all X Y Z Pid0 ((all V0 (-le_q(host(Pid0),V0)&le_q(s(zero),V0)->setIn(V0,index(down,host(Pid0)))|V0=host(Z)))&elem(m_Down(Z),queue(host(Pid0)))&host(Pid0)=host(Y)&host(Pid0)=nbr_proc&index(status,host(Pid0))=elec_1-> -(setIn(X,alive)&elem(m_Down(Y),queue(host(X))))))& (all X Y Z Pid0 (setIn(Pid0,alive)&elem(m_Down(Z),queue(host(Pid0)))&elem(m_Ack(Pid0,Y),queue(host(Pid0)))&le_q(nbr_proc,s(index(pendack,host(Pid0))))&index(status,host(Pid0))=elec_2&host(Y)=index(pendack,host(Pid0))&host(Z)=s(index(pendack,host(Pid0)))-> -(setIn(X,alive)&index(ldr,host(X))=host(X)&index(status,host(X))=norm)))-> (queue(host(W))=q_nil-> ((all X (host(W)=host(X)->le_q(X,V)))& -setIn(V,pids)&host(W)=host(V)-> (host(V)=s(zero)-> (-le_q(nbr_proc,host(V))-> (all X (host(V)!=host(X)-> (all Y Z Z0 (s(host(V))=host(Z0)-> (host(V)!=host(Z0)-> ((setIn(Z0,alive)|Z0=V)&le_q(nbr_proc,s(index(pendack,host(Z0))))&elem(m_Down(Z),snoc(queue(host(Z0)),m_Halt(V)))&elem(m_Ack(Z0,Y),snoc(queue(host(Z0)),m_Halt(V)))&index(status,host(Z0))=elec_2&host(Y)=index(pendack,host(Z0))&host(Z)=s(index(pendack,host(Z0)))-> -((setIn(X,alive)|X=V)&index(ldr,host(X))=host(X)&index(status,host(X))=norm))))))))))))). % 2.34/2.53 end_of_list. % 2.34/2.53 % 2.34/2.53 -------> usable clausifies to: % 2.34/2.53 % 2.34/2.53 list(usable). % 2.34/2.53 0 [] A=A. % 2.34/2.53 0 [] -elem(m_Ack(Pid,Pid2),queue(host(Pid)))|setIn(Pid,pids). % 2.34/2.53 0 [] -elem(m_Ack(Pid,Pid2),queue(host(Pid)))|setIn(Pid2,pids). % 2.34/2.53 0 [] s(host(P))!=host(Q)|host(P)!=host(Q). % 2.34/2.53 0 [] le_q(s(zero),host(P)). % 2.34/2.53 0 [] le_q(s(zero),nbr_proc). % 2.34/2.53 0 [] le_q(host(P),nbr_proc). % 2.34/2.53 0 [] elec_1!=elec_2. % 2.34/2.53 0 [] elec_1!=wait. % 2.34/2.53 0 [] elec_1!=norm. % 2.34/2.53 0 [] elec_2!=wait. % 2.34/2.53 0 [] elec_2!=norm. % 2.34/2.53 0 [] norm!=wait. % 2.34/2.53 0 [] m_Ack(X,Y)!=m_Halt(Z). % 2.34/2.53 0 [] m_Ack(X,Y)!=m_Down(Z). % 2.34/2.53 0 [] m_Ack(X,Y)!=m_NotNorm(Z). % 2.34/2.53 0 [] m_Ack(X,Y)!=m_Ldr(Z). % 2.34/2.53 0 [] m_Ack(X,Y)!=m_NormQ(Z). % 2.34/2.53 0 [] m_NotNorm(X)!=m_Halt(Y). % 2.34/2.53 0 [] m_Down(X)!=m_Halt(Y). % 2.34/2.53 0 [] m_Down(X)!=m_Ldr(Y). % 2.34/2.53 0 [] m_Down(X)!=m_NotNorm(Y). % 2.34/2.53 0 [] m_Down(X)!=m_NormQ(Y). % 2.34/2.53 0 [] m_NormQ(X)!=m_Halt(Y). % 2.34/2.53 0 [] m_Ldr(X)!=m_Halt(Y). % 2.34/2.53 0 [] m_Ldr(X)!=m_NormQ(Y). % 2.34/2.53 0 [] m_Ldr(X)!=m_NotNorm(Y). % 2.34/2.53 0 [] m_NormQ(X)!=m_NotNorm(Y). % 2.34/2.53 0 [] X=Y|m_Halt(X)!=m_Halt(Y). % 2.34/2.53 0 [] X!=Y|m_Halt(X)=m_Halt(Y). % 2.34/2.53 0 [] X=Y|m_NormQ(X)!=m_NormQ(Y). % 2.34/2.53 0 [] X!=Y|m_NormQ(X)=m_NormQ(Y). % 2.34/2.53 0 [] X=Y|m_NotNorm(X)!=m_NotNorm(Y). % 2.34/2.53 0 [] X!=Y|m_NotNorm(X)=m_NotNorm(Y). % 2.34/2.53 0 [] X=Y|m_Ldr(X)!=m_Ldr(Y). % 2.34/2.53 0 [] X!=Y|m_Ldr(X)=m_Ldr(Y). % 2.34/2.53 0 [] X=Y|m_Down(X)!=m_Down(Y). % 2.34/2.53 0 [] X!=Y|m_Down(X)=m_Down(Y). % 2.34/2.53 0 [] X1=X2|m_Ack(X1,Y1)!=m_Ack(X2,Y2). % 2.34/2.53 0 [] Y1=Y2|m_Ack(X1,Y1)!=m_Ack(X2,Y2). % 2.34/2.53 0 [] host(Pid)=host(Pid2)|Pid!=Pid2. % 2.34/2.53 0 [] -setIn(nil,alive). % 2.34/2.53 0 [] head(cons(X,Q))=X. % 2.34/2.53 0 [] tail(cons(X,Q))=Q. % 2.34/2.53 0 [] last(snoc(Q,Y))=Y. % 2.34/2.53 0 [] init(snoc(Q,Y))=Q. % 2.34/2.53 0 [] Q=q_nil|Q=cons(head(Q),tail(Q)). % 2.34/2.53 0 [] Q=q_nil|Q=snoc(init(Q),last(Q)). % 2.34/2.53 0 [] q_nil!=cons(X,Q). % 2.34/2.53 0 [] q_nil!=snoc(Q,Y). % 2.34/2.53 0 [] cons(X,q_nil)=snoc(q_nil,X). % 2.34/2.53 0 [] snoc(cons(X,Q),Y)=cons(X,snoc(Q,Y)). % 2.34/2.53 0 [] -elem(X,q_nil). % 2.34/2.53 0 [] -elem(X,cons(Y,Q))|X=Y|elem(X,Q). % 2.34/2.53 0 [] elem(X,cons(Y,Q))|X!=Y. % 2.34/2.53 0 [] elem(X,cons(Y,Q))| -elem(X,Q). % 2.34/2.53 0 [] -elem(X,snoc(Q,Y))|X=Y|elem(X,Q). % 2.34/2.53 0 [] elem(X,snoc(Q,Y))|X!=Y. % 2.34/2.53 0 [] elem(X,snoc(Q,Y))| -elem(X,Q). % 2.34/2.53 0 [] -pidElem(X)|X=m_Halt($f1(X))|X=m_Down($f1(X)). % 2.34/2.53 0 [] pidElem(X)|X!=m_Halt(Y). % 2.34/2.53 0 [] pidElem(X)|X!=m_Down(Y). % 2.34/2.53 0 [] pidMsg(m_Halt(X))=X. % 2.34/2.53 0 [] pidMsg(m_Down(X))=X. % 2.34/2.53 0 [] ordered(q_nil). % 2.34/2.53 0 [] ordered(cons(X,q_nil)). % 2.34/2.53 0 [] ordered(snoc(q_nil,X)). % 2.34/2.53 0 [] -ordered(cons(X,Q))|ordered(Q). % 2.34/2.53 0 [] -ordered(cons(X,Q))| -elem(Y,Q)| -pidElem(X)| -pidElem(Y)|host(pidMsg(Y))!=host(pidMsg(X))|le_q(pidMsg(X),pidMsg(Y)). % 2.34/2.53 0 [] ordered(cons(X,Q))| -ordered(Q)|elem($f2(X,Q),Q). % 2.34/2.53 0 [] ordered(cons(X,Q))| -ordered(Q)|pidElem(X). % 2.34/2.53 0 [] ordered(cons(X,Q))| -ordered(Q)|pidElem($f2(X,Q)). % 2.34/2.53 0 [] ordered(cons(X,Q))| -ordered(Q)|host(pidMsg($f2(X,Q)))=host(pidMsg(X)). % 2.34/2.53 0 [] ordered(cons(X,Q))| -ordered(Q)| -le_q(pidMsg(X),pidMsg($f2(X,Q))). % 2.34/2.53 0 [] -ordered(snoc(Q,X))|ordered(Q). % 2.34/2.53 0 [] -ordered(snoc(Q,X))| -elem(Y,Q)| -pidElem(X)| -pidElem(Y)|host(pidMsg(Y))!=host(pidMsg(X))|le_q(pidMsg(Y),pidMsg(X)). % 2.34/2.53 0 [] ordered(snoc(Q,X))| -ordered(Q)|elem($f3(X,Q),Q). % 2.34/2.53 0 [] ordered(snoc(Q,X))| -ordered(Q)|pidElem(X). % 2.34/2.53 0 [] ordered(snoc(Q,X))| -ordered(Q)|pidElem($f3(X,Q)). % 2.34/2.53 0 [] ordered(snoc(Q,X))| -ordered(Q)|host(pidMsg($f3(X,Q)))=host(pidMsg(X)). % 2.34/2.53 0 [] ordered(snoc(Q,X))| -ordered(Q)| -le_q(pidMsg($f3(X,Q)),pidMsg(X)). % 2.34/2.53 0 [] -ordered(Q)|ordered(snoc(Q,m_Ack(X,Y))). % 2.34/2.53 0 [] -ordered(Q)|ordered(snoc(Q,m_Ldr(X))). % 2.34/2.53 0 [] -ordered(cons(m_Halt(X),Q))|host(X)!=host(Y)| -elem(m_Down(Y),Q)|le_q(X,Y). % 2.34/2.53 0 [] -le_q(s(X),X). % 2.34/2.53 0 [] le_q(X,X). % 2.34/2.53 0 [] le_q(X,Y)|le_q(Y,X). % 2.34/2.53 0 [] -le_q(X,Y)| -le_q(Y,X)|X=Y. % 2.34/2.53 0 [] le_q(X,Y)|X!=Y. % 2.34/2.53 0 [] le_q(Y,X)|X!=Y. % 2.34/2.53 0 [] -le_q(X,Y)| -le_q(Y,Z)|le_q(X,Z). % 2.34/2.53 0 [] -le_q(X,Y)|le_q(s(X),s(Y)). % 2.34/2.53 0 [] le_q(X,Y)| -le_q(s(X),s(Y)). % 2.34/2.53 0 [] -le_q(X,s(Y))|X=s(Y)|le_q(X,Y). % 2.34/2.53 0 [] le_q(X,s(Y))|X!=s(Y). % 2.34/2.53 0 [] le_q(X,s(Y))| -le_q(X,Y). % 2.34/2.53 0 [] -setIn(X,setEmpty). % 2.34/2.53 0 [] host($c5)!=host(X)| -setIn(X,alive). % 2.34/2.53 0 [] -elem(m_Ldr(Y),queue(host(X3)))| -le_q(host(X3),host(Y)). % 2.34/2.53 0 [] -elem(m_Down(X5),queue(host(X4)))|host(X5)!=host(X4). % 2.34/2.53 0 [] -elem(m_Halt(X7),queue(host(X6)))| -le_q(host(X6),host(X7)). % 2.34/2.53 0 [] -elem(m_Ack(Z,X8),queue(host(X9)))| -le_q(host(X8),host(Z)). % 2.34/2.53 0 [] X11=X10|host(X11)!=host(X10)| -setIn(X10,alive)| -setIn(X11,alive). % 2.34/2.53 0 [] -setIn(X13,alive)| -elem(m_Ack(X13,X12),queue(host(X13)))|le_q(host(X12),index(pendack,host(X13))). % 2.34/2.53 0 [] -setIn(X15,alive)|index(status,host(X15))!=elec_1| -elem(m_Ack(X15,X14),queue(host(X15))). % 2.34/2.53 0 [] index(status,host(X16))!=elec_1| -setIn(X16,alive)|index(elid,host(X16))=X16. % 2.34/2.53 0 [] index(status,host(X16))!=elec_2| -setIn(X16,alive)|index(elid,host(X16))=X16. % 2.34/2.53 0 [] -setIn(X19,alive)| -elem(m_Down(X18),queue(host(X19)))|host(X18)!=host(X17)| -setIn(X17,alive)|index(ldr,host(X17))!=host(X17)|index(status,host(X17))!=norm. % 2.34/2.53 0 [] -setIn(X20,alive)| -setIn(X22,alive)|host(X22)!=host(X21)|index(status,host(X20))!=elec_2|index(status,host(X22))!=elec_2| -elem(m_Ack(X20,X21),queue(host(X20))). % 2.34/2.53 0 [] le_q(host(X23),host(X24))| -setIn(X23,alive)| -setIn(X24,alive)|index(status,host(X23))!=elec_2|index(status,host(X24))!=elec_2|le_q(index(pendack,host(X24)),host(X23)). % 2.34/2.53 0 [] le_q(host(X25),host(X26))| -setIn(X25,alive)| -setIn(X26,alive)|index(status,host(X25))!=elec_2|index(status,host(X26))!=elec_2| -le_q(index(pendack,host(X25)),index(pendack,host(X26))). % 2.34/2.53 0 [] le_q(index(pendack,host(X29)),host(X27))| -setIn(X29,alive)| -elem(m_Halt(X29),queue(host(X28)))|index(status,host(X29))!=elec_2| -setIn(X27,alive)|index(ldr,host(X27))!=host(X27)|index(status,host(X27))!=norm. % 2.34/2.53 0 [] -le_q(host(Pid0),$f4(X30,X31,X32,Pid0))| -elem(m_Down(X32),queue(host(Pid0)))|host(Pid0)!=host(X31)|host(Pid0)!=nbr_proc|index(status,host(Pid0))!=elec_1| -setIn(X30,alive)| -elem(m_Down(X31),queue(host(X30))). % 2.34/2.53 0 [] le_q(s(zero),$f4(X30,X31,X32,Pid0))| -elem(m_Down(X32),queue(host(Pid0)))|host(Pid0)!=host(X31)|host(Pid0)!=nbr_proc|index(status,host(Pid0))!=elec_1| -setIn(X30,alive)| -elem(m_Down(X31),queue(host(X30))). % 2.34/2.53 0 [] -setIn($f4(X30,X31,X32,Pid0),index(down,host(Pid0)))| -elem(m_Down(X32),queue(host(Pid0)))|host(Pid0)!=host(X31)|host(Pid0)!=nbr_proc|index(status,host(Pid0))!=elec_1| -setIn(X30,alive)| -elem(m_Down(X31),queue(host(X30))). % 2.34/2.53 0 [] $f4(X30,X31,X32,Pid0)!=host(X32)| -elem(m_Down(X32),queue(host(Pid0)))|host(Pid0)!=host(X31)|host(Pid0)!=nbr_proc|index(status,host(Pid0))!=elec_1| -setIn(X30,alive)| -elem(m_Down(X31),queue(host(X30))). % 2.34/2.53 0 [] -setIn(X36,alive)| -elem(m_Down(X35),queue(host(X36)))| -elem(m_Ack(X36,X34),queue(host(X36)))| -le_q(nbr_proc,s(index(pendack,host(X36))))|index(status,host(X36))!=elec_2|host(X34)!=index(pendack,host(X36))|host(X35)!=s(index(pendack,host(X36)))| -setIn(X33,alive)|index(ldr,host(X33))!=host(X33)|index(status,host(X33))!=norm. % 2.40/2.53 0 [] queue(host($c5))=q_nil. % 2.40/2.53 0 [] host($c5)!=host(X37)|le_q(X37,$c6). % 2.40/2.53 0 [] -setIn($c6,pids). % 2.40/2.53 0 [] host($c5)=host($c6). % 2.40/2.53 0 [] host($c6)=s(zero). % 2.40/2.53 0 [] -le_q(nbr_proc,host($c6)). % 2.40/2.53 0 [] host($c6)!=host($c4). % 2.40/2.53 0 [] s(host($c6))=host($c1). % 2.40/2.53 0 [] host($c6)!=host($c1). % 2.40/2.53 0 [] setIn($c1,alive)|$c1=$c6. % 2.40/2.53 0 [] le_q(nbr_proc,s(index(pendack,host($c1)))). % 2.40/2.53 0 [] elem(m_Down($c2),snoc(queue(host($c1)),m_Halt($c6))). % 2.40/2.53 0 [] elem(m_Ack($c1,$c3),snoc(queue(host($c1)),m_Halt($c6))). % 2.40/2.53 0 [] index(status,host($c1))=elec_2. % 2.40/2.53 0 [] host($c3)=index(pendack,host($c1)). % 2.40/2.53 0 [] host($c2)=s(index(pendack,host($c1))). % 2.40/2.53 0 [] setIn($c4,alive)|$c4=$c6. % 2.40/2.53 0 [] index(ldr,host($c4))=host($c4). % 2.40/2.53 0 [] index(status,host($c4))=norm. % 2.40/2.53 end_of_list. % 2.40/2.53 % 2.40/2.53 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=10. % 2.40/2.53 % 2.40/2.53 This ia a non-Horn set with equality. The strategy will be % 2.40/2.53 Knuth-Bendix, ordered hyper_res, factoring, and unit % 2.40/2.53 deletion, with positive clauses in sos and nonpositive % 2.40/2.53 clauses in usable. % 2.40/2.53 % 2.40/2.53 dependent: set(knuth_bendix). % 2.40/2.53 dependent: set(anl_eq). % 2.40/2.53 dependent: set(para_from). % 2.40/2.53 dependent: set(para_into). % 2.40/2.53 dependent: clear(para_from_right). % 2.40/2.53 dependent: clear(para_into_right). % 2.40/2.53 dependent: set(para_from_vars). % 2.40/2.53 dependent: set(eq_units_both_ways). % 2.40/2.53 dependent: set(dynamic_demod_all). % 2.40/2.53 dependent: set(dynamic_demod). % 2.40/2.53 dependent: set(order_eq). % 2.40/2.53 dependent: set(back_demod). % 2.40/2.53 dependent: set(lrpo). % 2.40/2.53 dependent: set(hyper_res). % 2.40/2.53 dependent: set(unit_deletion). % 2.40/2.53 dependent: set(factor). % 2.40/2.53 % 2.40/2.53 ------------> process usable: % 2.40/2.53 ** KEPT (pick-wt=10): 1 [] -elem(m_Ack(A,B),queue(host(A)))|setIn(A,pids). % 2.40/2.53 ** KEPT (pick-wt=10): 2 [] -elem(m_Ack(A,B),queue(host(A)))|setIn(B,pids). % 2.40/2.53 ** KEPT (pick-wt=11): 3 [] s(host(A))!=host(B)|host(A)!=host(B). % 2.40/2.53 ** KEPT (pick-wt=3): 5 [copy,4,flip.1] elec_2!=elec_1. % 2.40/2.53 ** KEPT (pick-wt=3): 7 [copy,6,flip.1] wait!=elec_1. % 2.40/2.53 ** KEPT (pick-wt=3): 9 [copy,8,flip.1] norm!=elec_1. % 2.40/2.53 ** KEPT (pick-wt=3): 11 [copy,10,flip.1] wait!=elec_2. % 2.40/2.53 ** KEPT (pick-wt=3): 13 [copy,12,flip.1] norm!=elec_2. % 2.40/2.53 ** KEPT (pick-wt=3): 15 [copy,14,flip.1] wait!=norm. % 2.40/2.53 ** KEPT (pick-wt=6): 16 [] m_Ack(A,B)!=m_Halt(C). % 2.40/2.53 ** KEPT (pick-wt=6): 17 [] m_Ack(A,B)!=m_Down(C). % 2.40/2.53 ** KEPT (pick-wt=6): 18 [] m_Ack(A,B)!=m_NotNorm(C). % 2.40/2.53 ** KEPT (pick-wt=6): 19 [] m_Ack(A,B)!=m_Ldr(C). % 2.40/2.53 ** KEPT (pick-wt=6): 20 [] m_Ack(A,B)!=m_NormQ(C). % 2.40/2.53 ** KEPT (pick-wt=5): 21 [] m_NotNorm(A)!=m_Halt(B). % 2.40/2.53 ** KEPT (pick-wt=5): 22 [] m_Down(A)!=m_Halt(B). % 2.40/2.53 ** KEPT (pick-wt=5): 23 [] m_Down(A)!=m_Ldr(B). % 2.40/2.53 ** KEPT (pick-wt=5): 24 [] m_Down(A)!=m_NotNorm(B). % 2.40/2.53 ** KEPT (pick-wt=5): 25 [] m_Down(A)!=m_NormQ(B). % 2.40/2.53 ** KEPT (pick-wt=5): 26 [] m_NormQ(A)!=m_Halt(B). % 2.40/2.53 ** KEPT (pick-wt=5): 27 [] m_Ldr(A)!=m_Halt(B). % 2.40/2.53 ** KEPT (pick-wt=5): 28 [] m_Ldr(A)!=m_NormQ(B). % 2.40/2.53 ** KEPT (pick-wt=5): 29 [] m_Ldr(A)!=m_NotNorm(B). % 2.40/2.53 ** KEPT (pick-wt=5): 30 [] m_NormQ(A)!=m_NotNorm(B). % 2.40/2.53 ** KEPT (pick-wt=8): 31 [] A=B|m_Halt(A)!=m_Halt(B). % 2.40/2.53 ** KEPT (pick-wt=8): 32 [] A!=B|m_Halt(A)=m_Halt(B). % 2.40/2.53 ** KEPT (pick-wt=8): 33 [] A=B|m_NormQ(A)!=m_NormQ(B). % 2.40/2.53 ** KEPT (pick-wt=8): 34 [] A!=B|m_NormQ(A)=m_NormQ(B). % 2.40/2.53 ** KEPT (pick-wt=8): 35 [] A=B|m_NotNorm(A)!=m_NotNorm(B). % 2.40/2.53 ** KEPT (pick-wt=8): 36 [] A!=B|m_NotNorm(A)=m_NotNorm(B). % 2.40/2.53 ** KEPT (pick-wt=8): 37 [] A=B|m_Ldr(A)!=m_Ldr(B). % 2.40/2.53 ** KEPT (pick-wt=8): 38 [] A!=B|m_Ldr(A)=m_Ldr(B). % 2.40/2.53 ** KEPT (pick-wt=8): 39 [] A=B|m_Down(A)!=m_Down(B). % 2.40/2.53 ** KEPT (pick-wt=8): 40 [] A!=B|m_Down(A)=m_Down(B). % 2.40/2.53 ** KEPT (pick-wt=10): 41 [] A=B|m_Ack(A,C)!=m_Ack(B,D). % 2.40/2.53 ** KEPT (pick-wt=10): 42 [] A=B|m_Ack(C,A)!=m_Ack(D,B). % 2.40/2.53 ** KEPT (pick-wt=8): 43 [] host(A)=host(B)|A!=B. % 2.40/2.53 ** KEPT (pick-wt=3): 44 [] -setIn(nil,alive). % 2.40/2.53 ** KEPT (pick-wt=5): 46 [copy,45,flip.1] cons(A,B)!=q_nil. % 2.40/2.53 ** KEPT (pick-wt=5): 48 [copy,47,flip.1] snoc(A,B)!=q_nil. % 2.40/2.53 ** KEPT (pick-wt=3): 49 [] -elem(A,q_nil). % 2.40/2.53 ** KEPT (pick-wt=11): 50 [] -elem(A,cons(B,C))|A=B|elem(A,C). % 2.40/2.53 ** KEPT (pick-wt=8): 51 [] elem(A,cons(B,C))|A!=B. % 2.40/2.53 ** KEPT (pick-wt=8): 52 [] elem(A,cons(B,C))| -elem(A,C). % 2.40/2.53 ** KEPT (pick-wt=11): 53 [] -elem(A,snoc(B,C))|A=C|elem(A,B). % 2.40/2.53 ** KEPT (pick-wt=8): 54 [] elem(A,snoc(B,C))|A!=C. % 2.40/2.53 ** KEPT (pick-wt=8): 55 [] elem(A,snoc(B,C))| -elem(A,B). % 2.40/2.54 ** KEPT (pick-wt=12): 57 [copy,56,flip.2,flip.3] -pidElem(A)|m_Halt($f1(A))=A|m_Down($f1(A))=A. % 2.40/2.54 ** KEPT (pick-wt=6): 58 [] pidElem(A)|A!=m_Halt(B). % 2.40/2.54 ** KEPT (pick-wt=6): 59 [] pidElem(A)|A!=m_Down(B). % 2.40/2.54 ** KEPT (pick-wt=6): 60 [] -ordered(cons(A,B))|ordered(B). % 2.40/2.54 ** KEPT (pick-wt=23): 61 [] -ordered(cons(A,B))| -elem(C,B)| -pidElem(A)| -pidElem(C)|host(pidMsg(C))!=host(pidMsg(A))|le_q(pidMsg(A),pidMsg(C)). % 2.40/2.54 ** KEPT (pick-wt=11): 62 [] ordered(cons(A,B))| -ordered(B)|elem($f2(A,B),B). % 2.40/2.54 ** KEPT (pick-wt=8): 63 [] ordered(cons(A,B))| -ordered(B)|pidElem(A). % 2.40/2.54 ** KEPT (pick-wt=10): 64 [] ordered(cons(A,B))| -ordered(B)|pidElem($f2(A,B)). % 2.40/2.54 ** KEPT (pick-wt=15): 65 [] ordered(cons(A,B))| -ordered(B)|host(pidMsg($f2(A,B)))=host(pidMsg(A)). % 2.40/2.54 ** KEPT (pick-wt=13): 66 [] ordered(cons(A,B))| -ordered(B)| -le_q(pidMsg(A),pidMsg($f2(A,B))). % 2.40/2.54 ** KEPT (pick-wt=6): 67 [] -ordered(snoc(A,B))|ordered(A). % 2.40/2.54 ** KEPT (pick-wt=23): 68 [] -ordered(snoc(A,B))| -elem(C,A)| -pidElem(B)| -pidElem(C)|host(pidMsg(C))!=host(pidMsg(B))|le_q(pidMsg(C),pidMsg(B)). % 2.40/2.54 ** KEPT (pick-wt=11): 69 [] ordered(snoc(A,B))| -ordered(A)|elem($f3(B,A),A). % 2.40/2.54 ** KEPT (pick-wt=8): 70 [] ordered(snoc(A,B))| -ordered(A)|pidElem(B). % 2.40/2.54 ** KEPT (pick-wt=10): 71 [] ordered(snoc(A,B))| -ordered(A)|pidElem($f3(B,A)). % 2.40/2.54 ** KEPT (pick-wt=15): 72 [] ordered(snoc(A,B))| -ordered(A)|host(pidMsg($f3(B,A)))=host(pidMsg(B)). % 2.40/2.54 ** KEPT (pick-wt=13): 73 [] ordered(snoc(A,B))| -ordered(A)| -le_q(pidMsg($f3(B,A)),pidMsg(B)). % 2.40/2.54 ** KEPT (pick-wt=8): 74 [] -ordered(A)|ordered(snoc(A,m_Ack(B,C))). % 2.40/2.54 ** KEPT (pick-wt=7): 75 [] -ordered(A)|ordered(snoc(A,m_Ldr(B))). % 2.40/2.54 ** KEPT (pick-wt=17): 76 [] -ordered(cons(m_Halt(A),B))|host(A)!=host(C)| -elem(m_Down(C),B)|le_q(A,C). % 2.40/2.54 ** KEPT (pick-wt=4): 77 [] -le_q(s(A),A). % 2.40/2.54 ** KEPT (pick-wt=9): 78 [] -le_q(A,B)| -le_q(B,A)|A=B. % 2.40/2.54 ** KEPT (pick-wt=6): 79 [] le_q(A,B)|A!=B. % 2.40/2.54 ** KEPT (pick-wt=6): 80 [] le_q(A,B)|B!=A. % 2.40/2.54 ** KEPT (pick-wt=9): 81 [] -le_q(A,B)| -le_q(B,C)|le_q(A,C). % 2.40/2.54 ** KEPT (pick-wt=8): 82 [] -le_q(A,B)|le_q(s(A),s(B)). % 2.40/2.54 ** KEPT (pick-wt=8): 83 [] le_q(A,B)| -le_q(s(A),s(B)). % 2.40/2.54 ** KEPT (pick-wt=11): 84 [] -le_q(A,s(B))|A=s(B)|le_q(A,B). % 2.40/2.54 Following clause subsumed by 79 during input processing: 0 [] le_q(A,s(B))|A!=s(B). % 2.40/2.54 ** KEPT (pick-wt=7): 85 [] le_q(A,s(B))| -le_q(A,B). % 2.40/2.54 ** KEPT (pick-wt=3): 86 [] -setIn(A,setEmpty). % 2.40/2.54 ** KEPT (pick-wt=8): 87 [] host($c5)!=host(A)| -setIn(A,alive). % 2.40/2.54 ** KEPT (pick-wt=11): 88 [] -elem(m_Ldr(A),queue(host(B)))| -le_q(host(B),host(A)). % 2.40/2.54 ** KEPT (pick-wt=11): 89 [] -elem(m_Down(A),queue(host(B)))|host(A)!=host(B). % 2.40/2.54 ** KEPT (pick-wt=11): 90 [] -elem(m_Halt(A),queue(host(B)))| -le_q(host(B),host(A)). % 2.40/2.54 ** KEPT (pick-wt=12): 91 [] -elem(m_Ack(A,B),queue(host(C)))| -le_q(host(B),host(A)). % 2.40/2.54 ** KEPT (pick-wt=14): 92 [] A=B|host(A)!=host(B)| -setIn(B,alive)| -setIn(A,alive). % 2.40/2.54 ** KEPT (pick-wt=17): 93 [] -setIn(A,alive)| -elem(m_Ack(A,B),queue(host(A)))|le_q(host(B),index(pendack,host(A))). % 2.40/2.54 ** KEPT (pick-wt=16): 94 [] -setIn(A,alive)|index(status,host(A))!=elec_1| -elem(m_Ack(A,B),queue(host(A))). % 2.40/2.54 ** KEPT (pick-wt=15): 95 [] index(status,host(A))!=elec_1| -setIn(A,alive)|index(elid,host(A))=A. % 2.40/2.54 ** KEPT (pick-wt=15): 96 [] index(status,host(A))!=elec_2| -setIn(A,alive)|index(elid,host(A))=A. % 2.40/2.54 ** KEPT (pick-wt=30): 97 [] -setIn(A,alive)| -elem(m_Down(B),queue(host(A)))|host(B)!=host(C)| -setIn(C,alive)|index(ldr,host(C))!=host(C)|index(status,host(C))!=norm. % 2.40/2.54 ** KEPT (pick-wt=30): 98 [] -setIn(A,alive)| -setIn(B,alive)|host(B)!=host(C)|index(status,host(A))!=elec_2|index(status,host(B))!=elec_2| -elem(m_Ack(A,C),queue(host(A))). % 2.40/2.54 ** KEPT (pick-wt=30): 99 [] le_q(host(A),host(B))| -setIn(A,alive)| -setIn(B,alive)|index(status,host(A))!=elec_2|index(status,host(B))!=elec_2|le_q(index(pendack,host(B)),host(A)). % 2.40/2.54 ** KEPT (pick-wt=32): 100 [] le_q(host(A),host(B))| -setIn(A,alive)| -setIn(B,alive)|index(status,host(A))!=elec_2|index(status,host(B))!=elec_2| -le_q(index(pendack,host(A)),index(pendack,host(B))). % 2.40/2.54 ** KEPT (pick-wt=38): 101 [] le_q(index(pendack,host(A)),host(B))| -setIn(A,alive)| -elem(m_Halt(A),queue(host(C)))|index(status,host(A))!=elec_2| -setIn(B,alive)|index(ldr,host(B))!=host(B)|index(status,host(B))!=norm. % 2.40/2.54 ** KEPT (pick-wt=38): 102 [] -le_q(host(A),$f4(B,C,D,A))| -elem(m_Down(D),queue(host(A)))|host(A)!=host(C)|host(A)!=nbr_proc|index(status,host(A))!=elec_1| -setIn(B,alive)| -elem(m_Down(C),queue(host(B))). % 2.40/2.54 ** KEPT (pick-wt=38): 103 [] le_q(s(zero),$f4(A,B,C,D))| -elem(m_Down(C),queue(host(D)))|host(D)!=host(B)|host(D)!=nbr_proc|index(status,host(D))!=elec_1| -setIn(A,alive)| -elem(m_Down(B),queue(host(A))). % 2.40/2.54 ** KEPT (pick-wt=40): 104 [] -setIn($f4(A,B,C,D),index(down,host(D)))| -elem(m_Down(C),queue(host(D)))|host(D)!=host(B)|host(D)!=nbr_proc|index(status,host(D))!=elec_1| -setIn(A,alive)| -elem(m_Down(B),queue(host(A))). % 2.40/2.54 ** KEPT (pick-wt=38): 105 [] $f4(A,B,C,D)!=host(C)| -elem(m_Down(C),queue(host(D)))|host(D)!=host(B)|host(D)!=nbr_proc|index(status,host(D))!=elec_1| -setIn(A,alive)| -elem(m_Down(B),queue(host(A))). % 2.40/2.54 ** KEPT (pick-wt=60): 106 [] -setIn(A,alive)| -elem(m_Down(B),queue(host(A)))| -elem(m_Ack(A,C),queue(host(A)))| -le_q(nbr_proc,s(index(pendack,host(A))))|index(status,host(A))!=elec_2|host(C)!=index(pendack,host(A))|host(B)!=s(index(pendack,host(A)))| -setIn(D,alive)|index(ldr,host(D))!=host(D)|index(status,host(D))!=norm. % 2.40/2.54 ** KEPT (pick-wt=8): 107 [] host($c5)!=host(A)|le_q(A,$c6). % 2.40/2.54 ** KEPT (pick-wt=3): 108 [] -setIn($c6,pids). % 2.40/2.54 ** KEPT (pick-wt=4): 109 [] -le_q(nbr_proc,host($c6)). % 2.40/2.54 ** KEPT (pick-wt=5): 110 [] host($c6)!=host($c4). % 2.40/2.54 ** KEPT (pick-wt=5): 111 [] host($c6)!=host($c1). % 2.40/2.54 ** KEPT (pick-wt=6): 112 [copy,16,flip.1] m_Halt(A)!=m_Ack(B,C). % 2.40/2.54 ** KEPT (pick-wt=6): 113 [copy,17,flip.1] m_Down(A)!=m_Ack(B,C). % 2.40/2.54 ** KEPT (pick-wt=6): 114 [copy,18,flip.1] m_NotNorm(A)!=m_Ack(B,C). % 2.40/2.54 ** KEPT (pick-wt=6): 115 [copy,19,flip.1] m_Ldr(A)!=m_Ack(B,C). % 2.40/2.54 ** KEPT (pick-wt=6): 116 [copy,20,flip.1] m_NormQ(A)!=m_Ack(B,C). % 2.40/2.54 ** KEPT (pick-wt=5): 117 [copy,21,flip.1] m_Halt(A)!=m_NotNorm(B). % 2.40/2.54 ** KEPT (pick-wt=5): 118 [copy,22,flip.1] m_Halt(A)!=m_Down(B). % 2.40/2.54 ** KEPT (pick-wt=5): 119 [copy,23,flip.1] m_Ldr(A)!=m_Down(B). % 2.40/2.54 ** KEPT (pick-wt=5): 120 [copy,24,flip.1] m_NotNorm(A)!=m_Down(B). % 2.40/2.54 ** KEPT (pick-wt=5): 121 [copy,25,flip.1] m_NormQ(A)!=m_Down(B). % 2.40/2.54 ** KEPT (pick-wt=5): 122 [copy,26,flip.1] m_Halt(A)!=m_NormQ(B). % 2.40/2.54 ** KEPT (pick-wt=5): 123 [copy,27,flip.1] m_Halt(A)!=m_Ldr(B). % 2.40/2.54 ** KEPT (pick-wt=5): 124 [copy,28,flip.1] m_NormQ(A)!=m_Ldr(B). % 2.40/2.54 ** KEPT (pick-wt=5): 125 [copy,29,flip.1] m_NotNorm(A)!=m_Ldr(B). % 2.40/2.54 ** KEPT (pick-wt=5): 126 [copy,30,flip.1] m_NotNorm(A)!=m_NormQ(B). % 2.40/2.54 Following clause subsumed by 16 during input processing: 0 [copy,112,flip.1] m_Ack(A,B)!=m_Halt(C). % 2.40/2.54 Following clause subsumed by 17 during input processing: 0 [copy,113,flip.1] m_Ack(A,B)!=m_Down(C). % 2.40/2.54 Following clause subsumed by 18 during input processing: 0 [copy,114,flip.1] m_Ack(A,B)!=m_NotNorm(C). % 2.40/2.54 Following clause subsumed by 19 during input processing: 0 [copy,115,flip.1] m_Ack(A,B)!=m_Ldr(C). % 2.40/2.54 Following clause subsumed by 20 during input processing: 0 [copy,116,flip.1] m_Ack(A,B)!=m_NormQ(C). % 2.40/2.54 Following clause subsumed by 21 during input processing: 0 [copy,117,flip.1] m_NotNorm(A)!=m_Halt(B). % 2.40/2.54 Following clause subsumed by 22 during input processing: 0 [copy,118,flip.1] m_Down(A)!=m_Halt(B). % 2.40/2.54 Following clause subsumed by 23 during input processing: 0 [copy,119,flip.1] m_Down(A)!=m_Ldr(B). % 2.40/2.54 Following clause subsumed by 24 during input processing: 0 [copy,120,flip.1] m_Down(A)!=m_NotNorm(B). % 2.40/2.54 Following clause subsumed by 25 during input processing: 0 [copy,121,flip.1] m_Down(A)!=m_NormQ(B). % 2.40/2.54 Following clause subsumed by 26 during input processing: 0 [copy,122,flip.1] m_NormQ(A)!=m_Halt(B). % 2.40/2.54 Following clause subsumed by 27 during input processing: 0 [copy,123,flip.1] m_Ldr(A)!=m_Halt(B). % 2.40/2.54 Following clause subsumed by 28 during input processing: 0 [copy,124,flip.1] m_Ldr(A)!=m_NormQ(B). % 2.40/2.54 Following clause subsumed by 29 during input processing: 0 [copy,125,flip.1] m_Ldr(A)!=m_NotNorm(B). % 2.40/2.54 Following clause subsumed by 30 during input processing: 0 [copy,126,flip.1] m_NormQ(A)!=m_NotNorm(B). % 2.40/2.54 % 2.40/2.54 ------------> process sos: % 2.40/2.54 ** KEPT (pick-wt=3): 140 [] A=A. % 2.40/2.54 ** KEPT (pick-wt=5): 141 [] le_q(s(zero),host(A)). % 2.40/2.54 ** KEPT (pick-wt=4): 142 [] le_q(s(zero),nbr_proc). % 2.40/2.54 ** KEPT (pick-wt=4): 143 [] le_q(host(A),nbr_proc). % 2.40/2.54 ** KEPT (pick-wt=6): 144 [] head(cons(A,B))=A. % 2.40/2.54 ---> New Demodulator: 145 [new_demod,144] head(cons(A,B))=A. % 2.40/2.54 ** KEPT (pick-wt=6): 146 [] tail(cons(A,B))=B. % 2.40/2.54 ---> New Demodulator: 147 [new_demod,146] tail(cons(A,B))=B. % 2.40/2.54 ** KEPT (pick-wt=6): 148 [] last(snoc(A,B))=B. % 2.40/2.54 ---> New Demodulator: 149 [new_demod,148] last(snoc(A,B))=B. % 2.40/2.54 ** KEPT (pick-wt=6): 150 [] init(snoc(A,B))=A. % 2.40/2.54 ---> New Demodulator: 151 [new_demod,150] init(snoc(A,B))=A. % 2.40/2.54 ** KEPT (pick-wt=10): 153 [copy,152,flip.2] A=q_nil|cons(head(A),tail(A))=A. % 2.40/2.54 ** KEPT (pick-wt=10): 155 [copy,154,flip.2] A=q_nil|snoc(init(A),last(A))=A. % 2.40/2.54 ** KEPT (pick-wt=7): 157 [copy,156,flip.1] snoc(q_nil,A)=cons(A,q_nil). % 2.40/2.54 ---> New Demodulator: 158 [new_demod,157] snoc(q_nil,A)=cons(A,q_nil). % 2.40/2.54 ** KEPT (pick-wt=11): 159 [] snoc(cons(A,B),C)=cons(A,snoc(B,C)). % 2.40/2.54 ---> New Demodulator: 160 [new_demod,159] snoc(cons(A,B),C)=cons(A,snoc(B,C)). % 2.40/2.54 ** KEPT (pick-wt=5): 161 [] pidMsg(m_Halt(A))=A. % 2.40/2.54 ---> New Demodulator: 162 [new_demod,161] pidMsg(m_Halt(A))=A. % 2.40/2.54 ** KEPT (pick-wt=5): 163 [] pidMsg(m_Down(A))=A. % 2.40/2.54 ---> New Demodulator: 164 [new_demod,163] pidMsg(m_Down(A))=A. % 2.40/2.54 ** KEPT (pick-wt=2): 165 [] ordered(q_nil). % 2.40/2.54 ** KEPT (pick-wt=4): 166 [] ordered(cons(A,q_nil)). % 2.40/2.54 Following clause subsumed by 166 during input processing: 0 [demod,158] ordered(cons(A,q_nil)). % 2.40/2.54 ** KEPT (pick-wt=3): 167 [] le_q(A,A). % 2.40/2.54 ** KEPT (pick-wt=6): 168 [] le_q(A,B)|le_q(B,A). % 2.40/2.54 ** KEPT (pick-wt=5): 169 [] queue(host($c5))=q_nil. % 2.40/2.54 ---> New Demodulator: 170 [new_demod,169] queue(host($c5))=q_nil. % 2.40/2.54 ** KEPT (pick-wt=5): 172 [copy,171,flip.1] host($c6)=host($c5). % 2.40/2.54 ---> New Demodulator: 173 [new_demod,172] host($c6)=host($c5). % 2.40/2.54 ** KEPT (pick-wt=5): 175 [copy,174,demod,173,flip.1] s(zero)=host($c5). % 2.40/2.54 ---> New Demodulator: 176 [new_demod,175] s(zero)=host($c5). % 2.40/2.54 ** KEPT (pick-wt=6): 178 [copy,177,demod,173] s(host($c5))=host($c1). % 2.40/2.54 ---> New Demodulator: 179 [new_demod,178] s(host($c5))=host($c1). % 2.40/2.54 ** KEPT (pick-wt=6): 181 [copy,180,flip.2] setIn($c1,alive)|$c6=$c1. % 2.40/2.54 ** KEPT (pick-wt=7): 182 [] le_q(nbr_proc,s(index(pendack,host($c1)))). % 2.40/2.54 ** KEPT (pick-wt=9): 183 [] elem(m_Down($c2),snoc(queue(host($c1)),m_Halt($c6))). % 2.40/2.54 ** KEPT (pick-wt=10): 184 [] elem(m_Ack($c1,$c3),snoc(queue(host($c1)),m_Halt($c6))). % 2.40/2.54 ** KEPT (pick-wt=6): 185 [] index(status,host($c1))=elec_2. % 2.40/2.54 ---> New Demodulator: 186 [new_demod,185] index(status,host($c1))=elec_2. % 2.40/2.54 ** KEPT (pick-wt=7): 187 [] host($c3)=index(pendack,host($c1)). % 2.40/2.54 ---> New Demodulator: 188 [new_demod,187] host($c3)=index(pendack,host($c1)). % 2.40/2.54 ** KEPT (pick-wt=8): 190 [copy,189,flip.1] s(index(pendack,host($c1)))=host($c2). % 2.40/2.54 ---> New Demodulator: 191 [new_demod,190] s(index(pendack,host($c1)))=host($c2). % 2.40/2.54 ** KEPT (pick-wt=6): 193 [copy,192,flip.2] setIn($c4,alive)|$c6=$c4. % 2.40/2.54 ** KEPT (pick-wt=7): 194 [] index(ldr,host($c4))=host($c4). % 2.40/2.54 ---> New Demodulator: 195 [new_demod,194] index(ldr,host($c4))=host($c4). % 2.40/2.54 ** KEPT (pick-wt=6): 196 [] index(status,host($c4))=norm. % 2.40/2.54 ---> New Demodulator: 197 [new_demod,196] index(status,host($c4))=norm. % 2.40/2.54 Following clause subsumed by 140 during input processing: 0 [copy,140,flip.1] A=A. % 2.40/2.54 140 back subsumes 130. % 2.40/2.54 140 back subsumes 129. % 2.40/2.54 >>>> Starting back demodulation with 145. % 2.40/2.54 >>>> Starting back demodulation with 147. % 2.40/2.54 >>>> Starting back demodulation with 149. % 2.40/2.54 >>>> Starting back demodulation with 151. % 2.40/2.54 >>>> Starting back demodulation with 158. % 2.40/2.54 >>>> Starting back demodulation with 160. % 2.40/2.54 >>>> Starting back demodulation with 162. % 2.40/2.54 >>>> Starting back demodulation with 164. % 2.40/2.54 167 back subsumes 133. % 2.40/2.54 167 back subsumes 132. % 2.40/2.54 167 back subsumes 128. % 2.40/2.54 167 back subsumes 127. % 2.40/2.54 >>>> Starting back demodulation with 170. % 2.40/2.54 >>>> Starting back demodulation with 173. % 2.40/2.54 >> back demodulating 111 with 173. % 2.40/2.54 >> back demodulating 110 with 173. % 2.40/2.54 >> back demodulating 109 with 173. % 2.40/2.54 >>>> Starting back demodulation with 176. % 2.40/2.54 >> back demodulating 142 with 176. % 2.40/2.54 >> back demodulating 141 with 176. % 2.40/2.54 >> back demodulating 136 with 176. % 2.40/2.54 >> back demodulating 103 with 176. % 2.40/2.54 >>>> Starting back demodulation with 179. % 26.63/26.80 >>>> Starting back demodulation with 186. % 26.63/26.80 >>>> Starting back demodulation with 188. % 26.63/26.80 >>>> Starting back demodulation with 191. % 26.63/26.80 >> back demodulating 182 with 191. % 26.63/26.80 >>>> Starting back demodulation with 195. % 26.63/26.80 >>>> Starting back demodulation with 197. % 26.63/26.80 % 26.63/26.80 ======= end of input processing ======= % 26.63/26.80 % 26.63/26.80 =========== start of search =========== % 26.63/26.80 % 26.63/26.80 % 26.63/26.80 Resetting weight limit to 8. % 26.63/26.80 % 26.63/26.80 % 26.63/26.80 Resetting weight limit to 8. % 26.63/26.80 % 26.63/26.80 sos_size=1149 % 26.63/26.80 % 26.63/26.80 % 26.63/26.80 Resetting weight limit to 7. % 26.63/26.80 % 26.63/26.80 % 26.63/26.80 Resetting weight limit to 7. % 26.63/26.80 % 26.63/26.80 sos_size=1268 % 26.63/26.80 % 26.63/26.80 Search stopped because sos empty. % 26.63/26.80 % 26.63/26.80 % 26.63/26.80 Search stopped because sos empty. % 26.63/26.80 % 26.63/26.80 ============ end of search ============ % 26.63/26.80 % 26.63/26.80 -------------- statistics ------------- % 26.63/26.80 clauses given 1601 % 26.63/26.80 clauses generated 1536940 % 26.63/26.80 clauses kept 1843 % 26.63/26.80 clauses forward subsumed 10030 % 26.63/26.80 clauses back subsumed 132 % 26.63/26.80 Kbytes malloced 10742 % 26.63/26.80 % 26.63/26.80 ----------- times (seconds) ----------- % 26.63/26.80 user CPU time 24.26 (0 hr, 0 min, 24 sec) % 26.63/26.80 system CPU time 0.01 (0 hr, 0 min, 0 sec) % 26.63/26.80 wall-clock time 26 (0 hr, 0 min, 26 sec) % 26.63/26.80 % 26.63/26.80 Process 12598 finished Wed Jul 27 06:27:14 2022 % 26.63/26.80 Otter interrupted % 26.63/26.80 PROOF NOT FOUND %------------------------------------------------------------------------------