import sympy as sp
t=sp.symbols("t")
A=1+t
Phi=1/(1+t)
B=-t*A*sp.diff(Phi,t)-A*Phi-t*sp.diff(A,t)*Phi
assert sp.simplify(B)==-1
print("FORMAL_EDGE_COUNTEREXAMPLE_PASS", sp.simplify(B))