[Top page]
Trying to prove with threshold = 0 1 --------------------------------- Ax --------------------------------- Ax q(Y),p(Y) --> p(Y),X#(p(X)/\q(X)) q(Y),p(Y) --> q(Y),X#(p(X)/\q(X)) ----------------------------------------------------------------------- R/\ q(Y),p(Y) --> p(Y)/\q(Y),X#(p(X)/\q(X)) --------------------------------------- R# q(Y),p(Y) --> X#(p(X)/\q(X)) ----------------------------- R~ p(Y) --> X#(p(X)/\q(X)),~q(Y) -------------------------------- R-> --> X#(p(X)/\q(X)),p(Y)-> ~q(Y) ------------------------------------ R@ --> X#(p(X)/\q(X)),X@(p(X)-> ~q(X)) ------------------------------------ L~ ~X#(p(X)/\q(X)) --> X@(p(X)-> ~q(X)) # Proved in 0 msec. Trying to prove with threshold = 0 1 ----------------------------------- Ax p(Y),q(Y),X@(p(X)-> ~q(X)) --> q(Y) ----------------------------------- Ax ------------------------------------- L~ p(Y),q(Y),X@(p(X)-> ~q(X)) --> p(Y) p(Y),q(Y),~q(Y),X@(p(X)-> ~q(X)) --> ----------------------------------------------------------------------------- L-> p(Y),q(Y),p(Y)-> ~q(Y),X@(p(X)-> ~q(X)) --> -------------------------------------------- L@ p(Y),q(Y),X@(p(X)-> ~q(X)) --> -------------------------------- L/\ p(Y)/\q(Y),X@(p(X)-> ~q(X)) --> ------------------------------------ L# X#(p(X)/\q(X)),X@(p(X)-> ~q(X)) --> ------------------------------------ R~ X@(p(X)-> ~q(X)) --> ~X#(p(X)/\q(X)) # Proved in 0 msec.