/usr/share/doc/prover9-doc/examples/bool-ring.in is in prover9-doc 0.0.200902a-2.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 | % A Boolean ring expression from a very old hardware analysis project.
(a2+b2+1+a2*b2)+ (a3+b3)+1+ (a0+b0+1+a0*b0)* (1+a0*b0)* (a1+b1+1+a1*b1)* (1+a1*b1)*
(a2+b2+1+a2*b2)* (1+a2*b2)* (cin+1)+ (a0+b0+1+a0*b0)* (1+a0*b0)* (a1+b1+1+a1*b1)*
(1+a1*b1)* (1+a2*b2)* (cin+1)+ (a0+b0+1+a0*b0)* (1+a0*b0)* (1+a1*b1)* (a2+b2+1+a2*b2)*
(1+a2*b2)* (cin+1)+ (a0+b0+1+a0*b0)* (1+a0*b0)* (1+a1*b1)* (1+a2*b2)*
(cin+1)+ (a0+b0+1+a0*b0)* (a1+b1+1+a1*b1)* (1+a1*b1)* (1+a2*b2)+ (a0+b0+1+a0*b0)*
(a1+b1+1+a1*b1)* (1+a1*b1)* (a2+b2+1+a2*b2)* (1+a2*b2)+ (a0+b0+1+a0*b0)* (1+a1*b1)*
(1+a2*b2)+ (a0+b0+1+a0*b0)* (1+a1*b1)* (a2+b2+1+a2*b2)* (1+a2*b2)+ (1+a0*b0)*
(a1+b1+1+a1*b1)* (1+a1*b1)* (a2+b2+1+a2*b2)* (1+a2*b2)* (cin+1)+ (1+a0*b0)*
(a1+b1+1+a1*b1)* (1+a1*b1)* (1+a2*b2)* (cin+1)+ (1+a0*b0)* (1+a1*b1)* (a2+b2+1+a2*b2)*
(1+a2*b2)* (cin+1)+ (1+a0*b0)* (1+a1*b1)* (1+a2*b2)* (cin+1)+ (a1+b1+1+a1*b1)*
(1+a2*b2)+ (a1+b1+1+a1*b1)* (a2+b2+1+a2*b2)* (1+a2*b2).
|