REDUCE
現在では Portable Standard Lisp (PSL)，Codemist Standard Lisp (CSL) ともopenになりましたので，気軽に比較できます．
最新版
mkdir ~/CAS export CAS=~/CAS cd $CAS svn co http://svn.code.sf.net/p/reduce-algebra/code/trunk reduce-algebra cd ./reduce-algebra ./configure --with-psl make ./configure --with-csl make cd ./generic/redfront make install echo "export PATH=$CAS/reduce-algebra/bin:$PATH" >> ~/.bashrc source ~/.bashrc redcsl -w --help rfcsl -h rfpsl -h
redcsl はデフォルトで GUI，-w オプションで端末モード（line editが可能）．
redpsl はデフォルトで 端末モード（line edit不可ですが，やや饒舌）．
一般にpslでコンパイルした後者の方が処理が高速と言われます．
rfpsl/csl は REDUCE front-end with psl/csl であり，rlwrap redcsl -w ではできなかった以前のセッションのコマンド履歴の参照が可能になります（履歴ファイルは ~/.reduce_history）．ただし，ctrl+z で落ちます．
rfcsl -v -b
Redfront 3.2/0, built 09-Aug-2013 ...
(C) 1999-2008 A. Dolzmann, 1999-2009 T. Sturm
Based on earlier projects by C. Cannam and W. Neun
Reports bugs to <http://sourceforge.net/forum/forum.php?forum_id=899364>
Codemist Standard Lisp 6.04 for linux-gnu:x86_64: Aug 9 2013
Created: Fri Aug 9 22:22:30 2013
Reduce (Free CSL version), 09-Aug-13 ...
Memory allocation: 117 Mbytes
Redfront learned 109 packages, 857 modules, 111 switches
1: load qepcad;on rlnzden,rladdcond,rlslfqvb;
3: rlqepcad ex({x,y},y=1/x and a*x+b*y=1);
4*a*b - 1 <= 0 and (a <> 0 or b <> 0)
4: rlqe ex({x,y,z},x^2+y^2+z^2=1 and a*x+b*y+c*z=1);
2
a - 1 = 0 or a + 1 = 0 or (c <> 0 and b = 0 and a <> 0 and a - 1 >= 0) or (
2 4 2 2 3 2 5 3
a <> 0 and 4*a - b - 2*b - 1 >= 0 and ((a *b - a *b - b + b <= 0
2 4 2 2 2 6 4 2 2
and a *b - 6*a *b + a + b + 2*b + b = 0 and (b*c > 0 or b *c - c >= 0))
2 3 2 5 3 2 4 2 2 2 6 4 2
or (a *b - a *b - b + b <= 0 and a *b - 6*a *b + a + b + 2*b + b = 0
2 2 3 2 5 3
and (b*c <= 0 or b *c - c <= 0)) or (a *b - a *b - b + b >= 0
2 4 2 2 2 6 4 2 2
and a *b - 6*a *b + a + b + 2*b + b = 0 and (b*c < 0 or b *c - c >= 0))
2 3 2 5 3 2 4 2 2 2 6 4 2
or (a *b - a *b - b + b >= 0 and a *b - 6*a *b + a + b + 2*b + b = 0
2
and (b*c >= 0 or b *c - c <= 0))) and (a - b = 0 or a + b = 0))
2
or (b = 0 and a <> 0 and a - 1 >= 0) or ((b <> 0 or a <> 0)
2 2
and (b = 0 or a + b - 1 >= 0) and ((
4 2 2 2 2
(a + a *b - a + b >= 0 or (b = 0 and a = 0)) and (((
4 2 3 2 3 4 2 2 2 2
(3*a *b + 3*a *b - 3*a *b + b >= 0 and (b = 0 or a + a *b - a - b <= 0))
5 3 3 3 3 4 2 2 2 2
or (a *b + a *b - a *b + 3*a*b >= 0 and (b = 0 or a + a *b - a - b >= 0))
4 2 2 2 2
) and (b*c > 0 or ((c <= 0 or b = 0 or a + a *b - a - b >= 0) and (a*c < 0
4 2 2 2 2
or ((c <= 0 or b = 0) and (c = 0 or b = 0 or a + a *b - a - b <= 0)))))) or
((
4 2 3 2 3 4 2 2 2 2
(3*a *b + 3*a *b - 3*a *b + b >= 0 and (b = 0 or a + a *b - a - b <= 0))
5 3 3 3 3 4 2 2 2 2
or (a *b + a *b - a *b + 3*a*b >= 0 and (b = 0 or a + a *b - a - b >= 0))
) and (b*c <= 0
4 2 2 2 2
or ((c >= 0 or b = 0) and (c = 0 or b = 0 or a + a *b - a - b <= 0))
4 2 2 2 2
or (a*c >= 0 and (c = 0 or b = 0 or a + a *b - a - b >= 0)))) or (
4 2 2 2 2 4 2 3 2 3
(b = 0 or a + a *b - a - b >= 0 or 3*a *b + 3*a *b - 3*a *b + b <= 0) and
5 3 3 3 3 4 2 3 2 3
(a *b + a *b - a *b + 3*a*b < 0 or (3*a *b + 3*a *b - 3*a *b + b <= 0
4 2 2 2 2
and (b = 0 or a + a *b - a - b <= 0))) and (b*c < 0 or (
4 2 2 2 2
(c <= 0 or b = 0 or a + a *b - a - b >= 0) and (a*c < 0
4 2 2 2 2
or ((c <= 0 or b = 0) and (c = 0 or b = 0 or a + a *b - a - b <= 0)))))) or
4 2 2 2 2 4 2 3 2 3
((b = 0 or a + a *b - a - b >= 0 or 3*a *b + 3*a *b - 3*a *b + b <= 0)
5 3 3 3 3 4 2 3 2 3
and (a *b + a *b - a *b + 3*a*b < 0 or (3*a *b + 3*a *b - 3*a *b + b <= 0
4 2 2 2 2
and (b = 0 or a + a *b - a - b <= 0))) and (b*c >= 0
4 2 2 2 2
or ((c >= 0 or b = 0) and (c = 0 or b = 0 or a + a *b - a - b <= 0))
4 2 2 2 2
or (a*c >= 0 and (c = 0 or b = 0 or a + a *b - a - b >= 0)))))) or (
4 2 2 2 2
(a + a *b - a + b >= 0 or (b = 0 and a = 0)) and (((
4 2 3 2 3 4 2 2 2 2
(3*a *b + 3*a *b - 3*a *b + b >= 0 and (b = 0 or a + a *b - a - b <= 0))
5 3 3 3 3 4 2 2 2 2
or (a *b + a *b - a *b + 3*a*b <= 0 and (b = 0 or a + a *b - a - b >= 0))
4 2 2 2 2
) and (b*c > 0 or ((c <= 0 or b = 0 or a + a *b - a - b >= 0) and (a*c > 0
4 2 2 2 2
or ((c <= 0 or b = 0) and (c = 0 or b = 0 or a + a *b - a - b <= 0)))))) or
((
4 2 3 2 3 4 2 2 2 2
(3*a *b + 3*a *b - 3*a *b + b >= 0 and (b = 0 or a + a *b - a - b <= 0))
5 3 3 3 3 4 2 2 2 2
or (a *b + a *b - a *b + 3*a*b <= 0 and (b = 0 or a + a *b - a - b >= 0))
) and (b*c <= 0
4 2 2 2 2
or ((c >= 0 or b = 0) and (c = 0 or b = 0 or a + a *b - a - b <= 0))
4 2 2 2 2
or (a*c <= 0 and (c = 0 or b = 0 or a + a *b - a - b >= 0)))) or (
4 2 2 2 2 4 2 3 2 3
(b = 0 or a + a *b - a - b >= 0 or 3*a *b + 3*a *b - 3*a *b + b <= 0) and
5 3 3 3 3 4 2 3 2 3
(a *b + a *b - a *b + 3*a*b > 0 or (3*a *b + 3*a *b - 3*a *b + b <= 0
4 2 2 2 2
and (b = 0 or a + a *b - a - b <= 0))) and (b*c < 0 or (
4 2 2 2 2
(c <= 0 or b = 0 or a + a *b - a - b >= 0) and (a*c > 0
4 2 2 2 2
or ((c <= 0 or b = 0) and (c = 0 or b = 0 or a + a *b - a - b <= 0)))))) or
4 2 2 2 2 4 2 3 2 3
((b = 0 or a + a *b - a - b >= 0 or 3*a *b + 3*a *b - 3*a *b + b <= 0)
5 3 3 3 3 4 2 3 2 3
and (a *b + a *b - a *b + 3*a*b > 0 or (3*a *b + 3*a *b - 3*a *b + b <= 0
4 2 2 2 2
and (b = 0 or a + a *b - a - b <= 0))) and (b*c >= 0
4 2 2 2 2
or ((c >= 0 or b = 0) and (c = 0 or b = 0 or a + a *b - a - b <= 0))
4 2 2 2 2
or (a*c <= 0 and (c = 0 or b = 0 or a + a *b - a - b >= 0))))))))
4 2
or (b = 0 and a <> 0 and a - a >= 0) or (b - c <> 0 and b + c <> 0 and a <> 0
2 2 2 2 4 2 2 2 8
and a *b - a *c + b + b *c = 0 and (c <> 0 or b <> 0) and (c = 0 or a *b
2 6 2 2 6 2 4 4 2 4 2 2 4 2 2 4
+ 2*a *b *c - 2*a *b + a *b *c + 4*a *b *c + a *b + 2*a *b *c
2 2 2 2 6 2 4 10 8 2 8 6 4 6 2 6
- 2*a *b *c - 4*a *c + a *c + b + 3*b *c - 2*b + 3*b *c - 2*b *c + b
4 6 4 4 4 2 2 6 2 4 6
+ b *c + 2*b *c - b *c + 2*b *c - b *c + c <= 0) and ((b*c <= 0 and (
2 10 2 8 2 2 8 2 6 4 2 6 2 2 6
c = 0 or a *b + 3*a *b *c - 2*a *b + 3*a *b *c + 6*a *b *c + a *b
2 4 6 2 4 4 2 4 2 2 2 6 2 2 4 2 6 12
+ a *b *c + 2*a *b *c - a *b *c - 6*a *b *c - a *b *c + a *c + b
10 2 10 8 4 8 2 8 6 6 6 4 6 2 4 6
+ 3*b *c - 2*b + 3*b *c - 2*b *c + b + b *c + 2*b *c - b *c + 2*b *c
4 4 2 6 6 4 2 5 2 3 5
- b *c + b *c <= 0)) or ((c = 0 or b *c + b *c - b *c - 2*b *c + c <= 0 or
2 10 2 8 2 2 8 2 6 4 2 6 2 2 6 2 4 6
a *b + 3*a *b *c - 2*a *b + 3*a *b *c + 6*a *b *c + a *b + a *b *c
2 4 4 2 4 2 2 2 6 2 2 4 2 6 12 10 2
+ 2*a *b *c - a *b *c - 6*a *b *c - a *b *c + a *c + b + 3*b *c
10 8 4 8 2 8 6 6 6 4 6 2 4 6 4 4
- 2*b + 3*b *c - 2*b *c + b + b *c + 2*b *c - b *c + 2*b *c - b *c
2 6 6 4 2 5 2 3 5
+ b *c <= 0) and (b*c > 0 or (b *c + b *c - b *c - 2*b *c + c <= 0 and (
2 10 2 8 2 2 8 2 6 4 2 6 2 2 6
c = 0 or a *b + 3*a *b *c - 2*a *b + 3*a *b *c + 6*a *b *c + a *b
2 4 6 2 4 4 2 4 2 2 2 6 2 2 4 2 6 12
+ a *b *c + 2*a *b *c - a *b *c - 6*a *b *c - a *b *c + a *c + b
10 2 10 8 4 8 2 8 6 6 6 4 6 2 4 6
+ 3*b *c - 2*b + 3*b *c - 2*b *c + b + b *c + 2*b *c - b *c + 2*b *c
4 4 2 6 6 4 2 5 2 3 5
- b *c + b *c >= 0)))) or (b *c + b *c - b *c - 2*b *c + c >= 0 and (c = 0
2 10 2 8 2 2 8 2 6 4 2 6 2 2 6 2 4 6
or a *b + 3*a *b *c - 2*a *b + 3*a *b *c + 6*a *b *c + a *b + a *b *c
2 4 4 2 4 2 2 2 6 2 2 4 2 6 12 10 2
+ 2*a *b *c - a *b *c - 6*a *b *c - a *b *c + a *c + b + 3*b *c
10 8 4 8 2 8 6 6 6 4 6 2 4 6 4 4
- 2*b + 3*b *c - 2*b *c + b + b *c + 2*b *c - b *c + 2*b *c - b *c
2 6 2 10 2 8 2 2 8
+ b *c >= 0)) or (b*c >= 0 and (c = 0 or a *b + 3*a *b *c - 2*a *b
2 6 4 2 6 2 2 6 2 4 6 2 4 4 2 4 2
+ 3*a *b *c + 6*a *b *c + a *b + a *b *c + 2*a *b *c - a *b *c
2 2 6 2 2 4 2 6 12 10 2 10 8 4 8 2
- 6*a *b *c - a *b *c + a *c + b + 3*b *c - 2*b + 3*b *c - 2*b *c
8 6 6 6 4 6 2 4 6 4 4 2 6
+ b + b *c + 2*b *c - b *c + 2*b *c - b *c + b *c <= 0)) or ((c = 0
6 4 2 5 2 3 5 2 10 2 8 2 2 8
or b *c + b *c - b *c - 2*b *c + c <= 0 or a *b + 3*a *b *c - 2*a *b
2 6 4 2 6 2 2 6 2 4 6 2 4 4 2 4 2
+ 3*a *b *c + 6*a *b *c + a *b + a *b *c + 2*a *b *c - a *b *c
2 2 6 2 2 4 2 6 12 10 2 10 8 4 8 2
- 6*a *b *c - a *b *c + a *c + b + 3*b *c - 2*b + 3*b *c - 2*b *c
8 6 6 6 4 6 2 4 6 4 4 2 6
+ b + b *c + 2*b *c - b *c + 2*b *c - b *c + b *c <= 0) and (b*c < 0 or
6 4 2 5 2 3 5 2 10 2 8 2
(b *c + b *c - b *c - 2*b *c + c <= 0 and (c = 0 or a *b + 3*a *b *c
2 8 2 6 4 2 6 2 2 6 2 4 6 2 4 4 2 4 2
- 2*a *b + 3*a *b *c + 6*a *b *c + a *b + a *b *c + 2*a *b *c - a *b *c
2 2 6 2 2 4 2 6 12 10 2 10 8 4 8 2
- 6*a *b *c - a *b *c + a *c + b + 3*b *c - 2*b + 3*b *c - 2*b *c
8 6 6 6 4 6 2 4 6 4 4 2 6
+ b + b *c + 2*b *c - b *c + 2*b *c - b *c + b *c >= 0))))))
2 2 2 2 2 2
or (b <> 0 and a <> 0 and a *b + a *c - b - c >= 0)
2 2 2 2 2 2
or (c <> 0 and a <> 0 and a *b + a *c - b - c >= 0) or ((b <> 0 or a <> 0)
2 2
and (b = 0 or a + b - 1 >= 0) and (((c <> 0 or b <> 0)
4 2 2 2 2
and (c = 0 or a + a *b - a + b >= 0 or (b = 0 and a = 0)) and (c = 0
4 2 2 2 2 4 2 2 2 2
or b = 0 or a + a *b - a + b >= 0 or (b >= 0 and a + a *b - a - b <= 0)
4 2 2 2 2
or (a*b >= 0 and a + a *b - a - b >= 0) or (
4 2 2 2 2
(b <= 0 or a + a *b - a - b >= 0)
4 2 2 2 2
and (a*b < 0 or (b <= 0 and a + a *b - a - b <= 0))))) or (
4 2 2 2 2
(c <> 0 or b <> 0) and (c = 0 or a + a *b - a + b >= 0 or (b = 0 and a = 0))
4 2 2 2 2
and (c = 0 or b = 0 or a + a *b - a + b >= 0
4 2 2 2 2
or (b >= 0 and a + a *b - a - b <= 0)
4 2 2 2 2
or (a*b <= 0 and a + a *b - a - b >= 0) or (
4 2 2 2 2
(b <= 0 or a + a *b - a - b >= 0)
4 2 2 2 2
and (a*b > 0 or (b <= 0 and a + a *b - a - b <= 0))))))) or (
2 2 2 2 4 2 2
a *b - a *c + b + b *c <> 0
2 4 2 4 6 4 2 4 2 4 4
and (b = 0 or a *b - a *c + b + 2*b *c - b + b *c + c >= 0) and ((
4 4 4 4 2 6 2 4 2 2 4
(c <> 0 or b <> 0) and (c = 0 or a *b - a *c + a *b + 2*a *b *c - a *b
2 2 4 2 4 6 4 2 2 4
+ a *b *c + a *c + b + 2*b *c + b *c <= 0) and ((b*c <= 0 and (c = 0
4 4 4 4 2 6 2 4 2 2 4 2 2 4 2 4 6
or b = 0 or a *b - a *c + a *b + 2*a *b *c - a *b + a *b *c + a *c + b
4 2 2 4 4 4 4 4 2 6
+ 2*b *c + b *c <= 0)) or ((c = 0 or b = 0 or a *b - a *c + a *b
2 4 2 2 4 2 2 4 2 4 6 4 2 2 4
+ 2*a *b *c - a *b + a *b *c + a *c + b + 2*b *c + b *c <= 0 or ((
2 4 2 5 6 4 3 2 5 4 4 4 4 2 6
a *b *c - a *c + b *c + 2*b *c + b *c <= 0 or a *b - a *c + a *b
2 4 2 2 4 2 2 4 2 4 6 4 2 2 4
+ 2*a *b *c - a *b + a *b *c + a *c - b - 2*b *c - b *c >= 0) and (
3 2 3 3 4 2 3
a *b *c - a *c + a*b *c + a*b *c < 0 or (
2 4 2 5 6 4 3 2 5 4 4 4 4 2 6
a *b *c - a *c + b *c + 2*b *c + b *c <= 0 and a *b - a *c + a *b
2 4 2 2 4 2 2 4 2 4 6 4 2 2 4
+ 2*a *b *c - a *b + a *b *c + a *c - b - 2*b *c - b *c <= 0)))) and (
2 4 2 5 6 4 3 2 5
b*c > 0 or ((c = 0 or b = 0 or a *b *c - a *c + b *c + 2*b *c + b *c <= 0 or
4 4 4 4 2 6 2 4 2 2 4 2 2 4 2 4 6 4 2
a *b - a *c + a *b + 2*a *b *c - a *b + a *b *c + a *c - b - 2*b *c
2 4 3 2 3 3 4 2 3
- b *c >= 0) and (a *b *c - a *c + a*b *c + a*b *c < 0 or (
2 4 2 5 6 4 3 2 5
(b = 0 or a *b *c - a *c + b *c + 2*b *c + b *c <= 0) and (c = 0 or b = 0 or
4 4 4 4 2 6 2 4 2 2 4 2 2 4 2 4 6 4 2
a *b - a *c + a *b + 2*a *b *c - a *b + a *b *c + a *c - b - 2*b *c
2 4 4 4 4 4 2 6 2 4 2
- b *c <= 0))) and (c = 0 or ((b = 0 or a *b - a *c + a *b + 2*a *b *c
2 4 2 2 4 2 4 6 4 2 2 4
- a *b + a *b *c + a *c + b + 2*b *c + b *c >= 0) and (b = 0
2 2 4 4 4 4 2 6 2 4 2 2 4 2 2 4
or a*b + a*c > 0 or a *b - a *c + a *b + 2*a *b *c - a *b + a *b *c
2 4 6 4 2 2 4
+ a *c + b + 2*b *c + b *c >= 0)))))) or (((
2 4 2 5 6 4 3 2 5
(b = 0 or a *b *c - a *c + b *c + 2*b *c + b *c >= 0) and (c = 0 or b = 0 or
4 4 4 4 2 6 2 4 2 2 4 2 2 4 2 4 6 4 2
a *b - a *c + a *b + 2*a *b *c - a *b + a *b *c + a *c - b - 2*b *c
2 4 3 2 3 3 4 2 3
- b *c <= 0)) or (a *b *c - a *c + a*b *c + a*b *c >= 0 and (c = 0 or b = 0
4 4 4 4 2 6 2 4 2 2 4 2 2 4 2 4 6 4 2
or a *b - a *c + a *b + 2*a *b *c - a *b + a *b *c + a *c - b - 2*b *c
2 4 4 4 4 4 2 6 2 4 2
- b *c >= 0))) and (c = 0 or ((b = 0 or a *b - a *c + a *b + 2*a *b *c
2 4 2 2 4 2 4 6 4 2 2 4
- a *b + a *b *c + a *c + b + 2*b *c + b *c >= 0) and (b = 0
2 2 4 4 4 4 2 6 2 4 2 2 4 2 2 4
or a*b + a*c > 0 or a *b - a *c + a *b + 2*a *b *c - a *b + a *b *c
2 4 6 4 2 2 4
+ a *c + b + 2*b *c + b *c >= 0)))) or (b*c >= 0 and (c = 0 or b = 0 or
4 4 4 4 2 6 2 4 2 2 4 2 2 4 2 4 6 4 2
a *b - a *c + a *b + 2*a *b *c - a *b + a *b *c + a *c + b + 2*b *c
2 4 4 4 4 4 2 6 2 4 2
+ b *c <= 0)) or ((c = 0 or b = 0 or a *b - a *c + a *b + 2*a *b *c
2 4 2 2 4 2 4 6 4 2 2 4
- a *b + a *b *c + a *c + b + 2*b *c + b *c <= 0 or ((
2 4 2 5 6 4 3 2 5 4 4 4 4 2 6
a *b *c - a *c + b *c + 2*b *c + b *c <= 0 or a *b - a *c + a *b
2 4 2 2 4 2 2 4 2 4 6 4 2 2 4
+ 2*a *b *c - a *b + a *b *c + a *c - b - 2*b *c - b *c >= 0) and (
3 2 3 3 4 2 3
a *b *c - a *c + a*b *c + a*b *c < 0 or (
2 4 2 5 6 4 3 2 5 4 4 4 4 2 6
a *b *c - a *c + b *c + 2*b *c + b *c <= 0 and a *b - a *c + a *b
2 4 2 2 4 2 2 4 2 4 6 4 2 2 4
+ 2*a *b *c - a *b + a *b *c + a *c - b - 2*b *c - b *c <= 0)))) and (
2 4 2 5 6 4 3 2 5
b*c < 0 or ((c = 0 or b = 0 or a *b *c - a *c + b *c + 2*b *c + b *c <= 0 or
4 4 4 4 2 6 2 4 2 2 4 2 2 4 2 4 6 4 2
a *b - a *c + a *b + 2*a *b *c - a *b + a *b *c + a *c - b - 2*b *c
2 4 3 2 3 3 4 2 3
- b *c >= 0) and (a *b *c - a *c + a*b *c + a*b *c < 0 or (
2 4 2 5 6 4 3 2 5
(b = 0 or a *b *c - a *c + b *c + 2*b *c + b *c <= 0) and (c = 0 or b = 0 or
4 4 4 4 2 6 2 4 2 2 4 2 2 4 2 4 6 4 2
a *b - a *c + a *b + 2*a *b *c - a *b + a *b *c + a *c - b - 2*b *c
2 4 4 4 4 4 2 6 2 4 2
- b *c <= 0))) and (c = 0 or ((b = 0 or a *b - a *c + a *b + 2*a *b *c
2 4 2 2 4 2 4 6 4 2 2 4
- a *b + a *b *c + a *c + b + 2*b *c + b *c >= 0) and (b = 0
2 2 4 4 4 4 2 6 2 4 2 2 4 2 2 4
or a*b + a*c > 0 or a *b - a *c + a *b + 2*a *b *c - a *b + a *b *c
2 4 6 4 2 2 4
+ a *c + b + 2*b *c + b *c >= 0)))))))) or ((c <> 0 or b <> 0) and (c = 0
4 4 4 4 2 6 2 4 2 2 4 2 2 4 2 4 6 4 2
or a *b - a *c + a *b + 2*a *b *c - a *b + a *b *c + a *c + b + 2*b *c
2 4 4 4 4 4 2 6
+ b *c <= 0) and ((b*c <= 0 and (c = 0 or b = 0 or a *b - a *c + a *b
2 4 2 2 4 2 2 4 2 4 6 4 2 2 4
+ 2*a *b *c - a *b + a *b *c + a *c + b + 2*b *c + b *c <= 0)) or ((
4 4 4 4 2 6 2 4 2 2 4 2 2 4 2 4
c = 0 or b = 0 or a *b - a *c + a *b + 2*a *b *c - a *b + a *b *c + a *c
6 4 2 2 4 2 4 2 5 6 4 3 2 5
+ b + 2*b *c + b *c <= 0 or ((a *b *c - a *c + b *c + 2*b *c + b *c <= 0
4 4 4 4 2 6 2 4 2 2 4 2 2 4 2 4 6 4 2
or a *b - a *c + a *b + 2*a *b *c - a *b + a *b *c + a *c - b - 2*b *c
2 4 3 2 3 3 4 2 3
- b *c >= 0) and (a *b *c - a *c + a*b *c + a*b *c > 0 or (
2 4 2 5 6 4 3 2 5 4 4 4 4 2 6
a *b *c - a *c + b *c + 2*b *c + b *c <= 0 and a *b - a *c + a *b
2 4 2 2 4 2 2 4 2 4 6 4 2 2 4
+ 2*a *b *c - a *b + a *b *c + a *c - b - 2*b *c - b *c <= 0)))) and (
2 4 2 5 6 4 3 2 5
b*c > 0 or ((c = 0 or b = 0 or a *b *c - a *c + b *c + 2*b *c + b *c <= 0 or
4 4 4 4 2 6 2 4 2 2 4 2 2 4 2 4 6 4 2
a *b - a *c + a *b + 2*a *b *c - a *b + a *b *c + a *c - b - 2*b *c
2 4 3 2 3 3 4 2 3
- b *c >= 0) and (a *b *c - a *c + a*b *c + a*b *c > 0 or (
2 4 2 5 6 4 3 2 5
(b = 0 or a *b *c - a *c + b *c + 2*b *c + b *c <= 0) and (c = 0 or b = 0 or
4 4 4 4 2 6 2 4 2 2 4 2 2 4 2 4 6 4 2
a *b - a *c + a *b + 2*a *b *c - a *b + a *b *c + a *c - b - 2*b *c
2 4 4 4 4 4 2 6 2 4 2
- b *c <= 0))) and (c = 0 or ((b = 0 or a *b - a *c + a *b + 2*a *b *c
2 4 2 2 4 2 4 6 4 2 2 4
- a *b + a *b *c + a *c + b + 2*b *c + b *c >= 0) and (b = 0
2 2 4 4 4 4 2 6 2 4 2 2 4 2 2 4
or a*b + a*c < 0 or a *b - a *c + a *b + 2*a *b *c - a *b + a *b *c
2 4 6 4 2 2 4
+ a *c + b + 2*b *c + b *c >= 0)))))) or (((
2 4 2 5 6 4 3 2 5
(b = 0 or a *b *c - a *c + b *c + 2*b *c + b *c >= 0) and (c = 0 or b = 0 or
4 4 4 4 2 6 2 4 2 2 4 2 2 4 2 4 6 4 2
a *b - a *c + a *b + 2*a *b *c - a *b + a *b *c + a *c - b - 2*b *c
2 4 3 2 3 3 4 2 3
- b *c <= 0)) or (a *b *c - a *c + a*b *c + a*b *c <= 0 and (c = 0 or b = 0
4 4 4 4 2 6 2 4 2 2 4 2 2 4 2 4 6 4 2
or a *b - a *c + a *b + 2*a *b *c - a *b + a *b *c + a *c - b - 2*b *c
2 4 4 4 4 4 2 6 2 4 2
- b *c >= 0))) and (c = 0 or ((b = 0 or a *b - a *c + a *b + 2*a *b *c
2 4 2 2 4 2 4 6 4 2 2 4
- a *b + a *b *c + a *c + b + 2*b *c + b *c >= 0) and (b = 0
2 2 4 4 4 4 2 6 2 4 2 2 4 2 2 4
or a*b + a*c < 0 or a *b - a *c + a *b + 2*a *b *c - a *b + a *b *c
2 4 6 4 2 2 4
+ a *c + b + 2*b *c + b *c >= 0)))) or (b*c >= 0 and (c = 0 or b = 0 or
4 4 4 4 2 6 2 4 2 2 4 2 2 4 2 4 6 4 2
a *b - a *c + a *b + 2*a *b *c - a *b + a *b *c + a *c + b + 2*b *c
2 4 4 4 4 4 2 6 2 4 2
+ b *c <= 0)) or ((c = 0 or b = 0 or a *b - a *c + a *b + 2*a *b *c
2 4 2 2 4 2 4 6 4 2 2 4
- a *b + a *b *c + a *c + b + 2*b *c + b *c <= 0 or ((
2 4 2 5 6 4 3 2 5 4 4 4 4 2 6
a *b *c - a *c + b *c + 2*b *c + b *c <= 0 or a *b - a *c + a *b
2 4 2 2 4 2 2 4 2 4 6 4 2 2 4
+ 2*a *b *c - a *b + a *b *c + a *c - b - 2*b *c - b *c >= 0) and (
3 2 3 3 4 2 3
a *b *c - a *c + a*b *c + a*b *c > 0 or (
2 4 2 5 6 4 3 2 5 4 4 4 4 2 6
a *b *c - a *c + b *c + 2*b *c + b *c <= 0 and a *b - a *c + a *b
2 4 2 2 4 2 2 4 2 4 6 4 2 2 4
+ 2*a *b *c - a *b + a *b *c + a *c - b - 2*b *c - b *c <= 0)))) and (
2 4 2 5 6 4 3 2 5
b*c < 0 or ((c = 0 or b = 0 or a *b *c - a *c + b *c + 2*b *c + b *c <= 0 or
4 4 4 4 2 6 2 4 2 2 4 2 2 4 2 4 6 4 2
a *b - a *c + a *b + 2*a *b *c - a *b + a *b *c + a *c - b - 2*b *c
2 4 3 2 3 3 4 2 3
- b *c >= 0) and (a *b *c - a *c + a*b *c + a*b *c > 0 or (
2 4 2 5 6 4 3 2 5
(b = 0 or a *b *c - a *c + b *c + 2*b *c + b *c <= 0) and (c = 0 or b = 0 or
4 4 4 4 2 6 2 4 2 2 4 2 2 4 2 4 6 4 2
a *b - a *c + a *b + 2*a *b *c - a *b + a *b *c + a *c - b - 2*b *c
2 4 4 4 4 4 2 6 2 4 2
- b *c <= 0))) and (c = 0 or ((b = 0 or a *b - a *c + a *b + 2*a *b *c
2 4 2 2 4 2 4 6 4 2 2 4
- a *b + a *b *c + a *c + b + 2*b *c + b *c >= 0) and (b = 0
2 2 4 4 4 4 2 6 2 4 2 2 4 2 2 4
or a*b + a*c < 0 or a *b - a *c + a *b + 2*a *b *c - a *b + a *b *c
2 4 6 4 2 2 4
+ a *c + b + 2*b *c + b *c >= 0)))))))))) or (
2 2
(b <> 0 or (c <> 0 and a <> 0)) and (b = 0 or a + b - 1 >= 0) and ((
4 2 2 2 2
(c <> 0 or b <> 0) and (c = 0 or a + a *b - a + b >= 0 or (b = 0 and a = 0))
4 2 2 2 2
and (c = 0 or b = 0 or a + a *b - a + b >= 0 or (
3 2 4 2 2 2 2
(b + b*c <= 0 or a + a *b - a - b >= 0)
3 2 4 2 2 2 2
and (a*b < 0 or (b + b*c <= 0 and a + a *b - a - b <= 0)))
3 2 4 2 2 2 2
or (b + b*c >= 0 and a + a *b - a - b <= 0)
4 2 2 2 2
or (a*b >= 0 and a + a *b - a - b >= 0))) or ((c <> 0 or b <> 0)
4 2 2 2 2
and (c = 0 or a + a *b - a + b >= 0 or (b = 0 and a = 0)) and (c = 0
4 2 2 2 2
or b = 0 or a + a *b - a + b >= 0 or (
3 2 4 2 2 2 2
(b + b*c <= 0 or a + a *b - a - b >= 0)
3 2 4 2 2 2 2
and (a*b > 0 or (b + b*c <= 0 and a + a *b - a - b <= 0)))
3 2 4 2 2 2 2
or (b + b*c >= 0 and a + a *b - a - b <= 0)
4 2 2 2 2
or (a*b <= 0 and a + a *b - a - b >= 0))))) or (
2 2 2 2 4 2 2 2 4 2
a *b + a *c + b + 2*b *c - b + c - c >= 0
and (c <> 0 or b <> 0 or a <> 0) and (((c <> 0 or b <> 0) and (((c = 0 or
4 2 4 2 2 4 2 2 2 2 2 2 4 2 2 4 2 2 4
a *b + a *c + a *b + 2*a *b *c - a *b + a *c - a *c + b + 2*b *c + c
2 3
>= 0) and ((((b *c + c >= 0 and (c = 0 or
4 2 4 2 2 4 2 2 2 2 2 2 4 2 2 4 2 2 4
a *b + a *c + a *b + 2*a *b *c - a *b + a *c - a *c - b - 2*b *c - c
<= 0)) or (a*c >= 0 and (c = 0 or
4 2 4 2 2 4 2 2 2 2 2 2 4 2 2 4 2 2 4
a *b + a *c + a *b + 2*a *b *c - a *b + a *c - a *c - b - 2*b *c - c
>= 0))) and (c = 0 or
4 2 4 2 2 4 2 2 2 2 2 2 4 2 2 4 2 2 4
a *b + a *c + a *b + 2*a *b *c - a *b + a *c - a *c + b + 2*b *c + c
>= 0)) or (b*c >= 0 and (c = 0 or
4 2 4 2 2 4 2 2 2 2 2 2 4 2 2 4 2 2 4
a *b + a *c + a *b + 2*a *b *c - a *b + a *c - a *c + b + 2*b *c + c
<= 0)) or ((c = 0 or
4 2 4 2 2 4 2 2 2 2 2 2 4 2 2 4 2 2 4
a *b + a *c + a *b + 2*a *b *c - a *b + a *c - a *c + b + 2*b *c + c
2 3
<= 0 or ((b *c + c <= 0 or
4 2 4 2 2 4 2 2 2 2 2 2 4 2 2 4 2 2 4
a *b + a *c + a *b + 2*a *b *c - a *b + a *c - a *c - b - 2*b *c - c
2 3
>= 0) and (a*c < 0 or (b *c + c <= 0 and
4 2 4 2 2 4 2 2 2 2 2 2 4 2 2 4 2 2 4
a *b + a *c + a *b + 2*a *b *c - a *b + a *c - a *c - b - 2*b *c - c
2 3
<= 0)))) and (b*c < 0 or ((c = 0 or b *c + c <= 0 or
4 2 4 2 2 4 2 2 2 2 2 2 4 2 2 4 2 2 4
a *b + a *c + a *b + 2*a *b *c - a *b + a *c - a *c - b - 2*b *c - c
2 3
>= 0) and (a*c < 0 or (b *c + c <= 0 and (c = 0 or
4 2 4 2 2 4 2 2 2 2 2 2 4 2 2 4 2 2 4
a *b + a *c + a *b + 2*a *b *c - a *b + a *c - a *c - b - 2*b *c - c
<= 0))) and (c = 0 or
4 2 4 2 2 4 2 2 2 2 2 2 4 2 2 4 2 2 4
a *b + a *c + a *b + 2*a *b *c - a *b + a *c - a *c + b + 2*b *c + c
>= 0)))))) or ((c = 0 or
4 2 4 2 2 4 2 2 2 2 2 2 4 2 2 4 2 2 4
a *b + a *c + a *b + 2*a *b *c - a *b + a *c - a *c + b + 2*b *c + c
2 3
>= 0) and ((((b *c + c >= 0 and (c = 0 or
4 2 4 2 2 4 2 2 2 2 2 2 4 2 2 4 2 2 4
a *b + a *c + a *b + 2*a *b *c - a *b + a *c - a *c - b - 2*b *c - c
<= 0)) or (a*c >= 0 and (c = 0 or
4 2 4 2 2 4 2 2 2 2 2 2 4 2 2 4 2 2 4
a *b + a *c + a *b + 2*a *b *c - a *b + a *c - a *c - b - 2*b *c - c
>= 0))) and (c = 0 or
4 2 4 2 2 4 2 2 2 2 2 2 4 2 2 4 2 2 4
a *b + a *c + a *b + 2*a *b *c - a *b + a *c - a *c + b + 2*b *c + c
>= 0)) or (b*c <= 0 and (c = 0 or
4 2 4 2 2 4 2 2 2 2 2 2 4 2 2 4 2 2 4
a *b + a *c + a *b + 2*a *b *c - a *b + a *c - a *c + b + 2*b *c + c
<= 0)) or ((c = 0 or
4 2 4 2 2 4 2 2 2 2 2 2 4 2 2 4 2 2 4
a *b + a *c + a *b + 2*a *b *c - a *b + a *c - a *c + b + 2*b *c + c
2 3
<= 0 or ((b *c + c <= 0 or
4 2 4 2 2 4 2 2 2 2 2 2 4 2 2 4 2 2 4
a *b + a *c + a *b + 2*a *b *c - a *b + a *c - a *c - b - 2*b *c - c
2 3
>= 0) and (a*c < 0 or (b *c + c <= 0 and
4 2 4 2 2 4 2 2 2 2 2 2 4 2 2 4 2 2 4
a *b + a *c + a *b + 2*a *b *c - a *b + a *c - a *c - b - 2*b *c - c
2 3
<= 0)))) and (b*c > 0 or ((c = 0 or b *c + c <= 0 or
4 2 4 2 2 4 2 2 2 2 2 2 4 2 2 4 2 2 4
a *b + a *c + a *b + 2*a *b *c - a *b + a *c - a *c - b - 2*b *c - c
2 3
>= 0) and (a*c < 0 or (b *c + c <= 0 and (c = 0 or
4 2 4 2 2 4 2 2 2 2 2 2 4 2 2 4 2 2 4
a *b + a *c + a *b + 2*a *b *c - a *b + a *c - a *c - b - 2*b *c - c
<= 0))) and (c = 0 or
4 2 4 2 2 4 2 2 2 2 2 2 4 2 2 4 2 2 4
a *b + a *c + a *b + 2*a *b *c - a *b + a *c - a *c + b + 2*b *c + c
>= 0)))))))) or ((c <> 0 or b <> 0) and (((c = 0 or
4 2 4 2 2 4 2 2 2 2 2 2 4 2 2 4 2 2 4
a *b + a *c + a *b + 2*a *b *c - a *b + a *c - a *c + b + 2*b *c + c
2 3
>= 0) and ((((b *c + c >= 0 and (c = 0 or
4 2 4 2 2 4 2 2 2 2 2 2 4 2 2 4 2 2 4
a *b + a *c + a *b + 2*a *b *c - a *b + a *c - a *c - b - 2*b *c - c
<= 0)) or (a*c <= 0 and (c = 0 or
4 2 4 2 2 4 2 2 2 2 2 2 4 2 2 4 2 2 4
a *b + a *c + a *b + 2*a *b *c - a *b + a *c - a *c - b - 2*b *c - c
>= 0))) and (c = 0 or
4 2 4 2 2 4 2 2 2 2 2 2 4 2 2 4 2 2 4
a *b + a *c + a *b + 2*a *b *c - a *b + a *c - a *c + b + 2*b *c + c
>= 0)) or (b*c >= 0 and (c = 0 or
4 2 4 2 2 4 2 2 2 2 2 2 4 2 2 4 2 2 4
a *b + a *c + a *b + 2*a *b *c - a *b + a *c - a *c + b + 2*b *c + c
<= 0)) or ((c = 0 or
4 2 4 2 2 4 2 2 2 2 2 2 4 2 2 4 2 2 4
a *b + a *c + a *b + 2*a *b *c - a *b + a *c - a *c + b + 2*b *c + c
2 3
<= 0 or ((b *c + c <= 0 or
4 2 4 2 2 4 2 2 2 2 2 2 4 2 2 4 2 2 4
a *b + a *c + a *b + 2*a *b *c - a *b + a *c - a *c - b - 2*b *c - c
2 3
>= 0) and (a*c > 0 or (b *c + c <= 0 and
4 2 4 2 2 4 2 2 2 2 2 2 4 2 2 4 2 2 4
a *b + a *c + a *b + 2*a *b *c - a *b + a *c - a *c - b - 2*b *c - c
2 3
<= 0)))) and (b*c < 0 or ((c = 0 or b *c + c <= 0 or
4 2 4 2 2 4 2 2 2 2 2 2 4 2 2 4 2 2 4
a *b + a *c + a *b + 2*a *b *c - a *b + a *c - a *c - b - 2*b *c - c
2 3
>= 0) and (a*c > 0 or (b *c + c <= 0 and (c = 0 or
4 2 4 2 2 4 2 2 2 2 2 2 4 2 2 4 2 2 4
a *b + a *c + a *b + 2*a *b *c - a *b + a *c - a *c - b - 2*b *c - c
<= 0))) and (c = 0 or
4 2 4 2 2 4 2 2 2 2 2 2 4 2 2 4 2 2 4
a *b + a *c + a *b + 2*a *b *c - a *b + a *c - a *c + b + 2*b *c + c
>= 0)))))) or ((c = 0 or
4 2 4 2 2 4 2 2 2 2 2 2 4 2 2 4 2 2 4
a *b + a *c + a *b + 2*a *b *c - a *b + a *c - a *c + b + 2*b *c + c
2 3
>= 0) and ((((b *c + c >= 0 and (c = 0 or
4 2 4 2 2 4 2 2 2 2 2 2 4 2 2 4 2 2 4
a *b + a *c + a *b + 2*a *b *c - a *b + a *c - a *c - b - 2*b *c - c
<= 0)) or (a*c <= 0 and (c = 0 or
4 2 4 2 2 4 2 2 2 2 2 2 4 2 2 4 2 2 4
a *b + a *c + a *b + 2*a *b *c - a *b + a *c - a *c - b - 2*b *c - c
>= 0))) and (c = 0 or
4 2 4 2 2 4 2 2 2 2 2 2 4 2 2 4 2 2 4
a *b + a *c + a *b + 2*a *b *c - a *b + a *c - a *c + b + 2*b *c + c
>= 0)) or (b*c <= 0 and (c = 0 or
4 2 4 2 2 4 2 2 2 2 2 2 4 2 2 4 2 2 4
a *b + a *c + a *b + 2*a *b *c - a *b + a *c - a *c + b + 2*b *c + c
<= 0)) or ((c = 0 or
4 2 4 2 2 4 2 2 2 2 2 2 4 2 2 4 2 2 4
a *b + a *c + a *b + 2*a *b *c - a *b + a *c - a *c + b + 2*b *c + c
2 3
<= 0 or ((b *c + c <= 0 or
4 2 4 2 2 4 2 2 2 2 2 2 4 2 2 4 2 2 4
a *b + a *c + a *b + 2*a *b *c - a *b + a *c - a *c - b - 2*b *c - c
2 3
>= 0) and (a*c > 0 or (b *c + c <= 0 and
4 2 4 2 2 4 2 2 2 2 2 2 4 2 2 4 2 2 4
a *b + a *c + a *b + 2*a *b *c - a *b + a *c - a *c - b - 2*b *c - c
2 3
<= 0)))) and (b*c > 0 or ((c = 0 or b *c + c <= 0 or
4 2 4 2 2 4 2 2 2 2 2 2 4 2 2 4 2 2 4
a *b + a *c + a *b + 2*a *b *c - a *b + a *c - a *c - b - 2*b *c - c
2 3
>= 0) and (a*c > 0 or (b *c + c <= 0 and (c = 0 or
4 2 4 2 2 4 2 2 2 2 2 2 4 2 2 4 2 2 4
a *b + a *c + a *b + 2*a *b *c - a *b + a *c - a *c - b - 2*b *c - c
<= 0))) and (c = 0 or
4 2 4 2 2 4 2 2 2 2 2 2 4 2 2 4 2 2 4
a *b + a *c + a *b + 2*a *b *c - a *b + a *c - a *c + b + 2*b *c + c
2 2
>= 0)))))))))) or (c <> 0 and b <> 0 and a + b - 1 >= 0)
5: rlslfq ws;
+ The input formula is: The OR of 15 things!
+ It contains 580 atomic formulas, nested to a depth of 13.
+ Variables are: b,c,a
+ Cutoff is 2
+ Simplifying disjunct number 1
+ Subformula 1:
+ a - 1 = 0
+ Simplifying disjunct number 2
+ Subformula 2:
+ a + 1 = 0
+ Simplifying disjunct number 3
+ Subformula 3:
+ [ b = 0 /\ c /= 0 /\ [ a - 1 >= 0 \/ a + 1 <= 0 ] ]
+ Simplifying disjunct number 4
+ Subformula 4:
+ [ b - 1 <= 0 /\ b + 1 >= 0 /\ b^4 a^2 - 6 b^2 a^2 + a^2 + b^6 + 2 b^4 + b^2 = 0 /\ [ b - 1 = 0 \/ b + 1 = 0 ] ]
+ Simplifying disjunct number 5
+ Subformula 5:
+ [ b = 0 /\ [ a - 1 >= 0 \/ a + 1 <= 0 ] ]
+ Simplifying disjunct number 6
+ Subformula 6:
+ a^2 + b^2 - 1 >= 0
+ Simplifying disjunct number 7
+ Subformula 7:
+ [ b = 0 /\ [ a - 1 >= 0 \/ a + 1 <= 0 ] ]
+ Simplifying disjunct number 8
+ Subformula 8:
+ [ c - b /= 0 /\ b^2 c^2 - c^2 + b^4 + b^2 = 0 /\ c^2 a^2 - b^2 a^2 - b^2 c^2 - b^4 = 0 ]
+ Simplifying disjunct number 9
+ Subformula 9:
+ [ b /= 0 /\ [ a - 1 >= 0 \/ a + 1 <= 0 ] ]
+ Simplifying disjunct number 10
+ Subformula 10:
+ [ c /= 0 /\ [ a - 1 >= 0 \/ a + 1 <= 0 ] ]
+ Simplifying disjunct number 11
+ Subformula 11:
+ [ a^2 + b^2 - 1 >= 0 /\ [ b /= 0 \/ c /= 0 ] ]
+ Simplifying disjunct number 12
+ Subformula 12:
+ [ c - b /= 0 /\ [ [ b = 0 /\ c^2 a^2 - b^2 a^2 - b^2 c^2 - c^2 - b^4 + b^2 >= 0 ] \/ [ c = 0 /\ c^2 a^2 - b^2 a^2 - b^2 c^2 - c^2 - b^4 + b^2 <= 0 ] ] ]
+ Simplifying disjunct number 13
+ Subformula 13:
+ [ a^2 + b^2 - 1 >= 0 /\ [ b /= 0 \/ c /= 0 ] ]
+ Simplifying disjunct number 14
+ Subformula 14:
+ [ c^2 + b^2 > 0 /\ a^2 + c^2 + b^2 - 1 >= 0 ]
+ Simplifying disjunct number 15
+ Subformula 15:
+ [ b /= 0 /\ c /= 0 /\ a^2 + b^2 - 1 >= 0 ]
+
+
+ ===================== The End =======================
+
+ -----------------------------------------------------------------------------
+ 25 Garbage collections, 60177628 Cells and 3 Arrays reclaimed, in 480 milliseconds.
+ 2156108 Cells in AVAIL, 2500000 Cells in SPACE.
+
+ System time: 10100 milliseconds.
+ System time after the initialization: 10092 milliseconds.
+ -----------------------------------------------------------------------------
+ An equivalent formula is:
+ a^2 + c^2 + b^2 - 1 >= 0
+ There were 1143 QEPCADB calls!
2 2 2
a + b + c - 1 >= 0
6: rlqepcadn 100000000;
7: rlqepcad ex({x,y,z},x^2+y^2+z^2=1 and a*x+b*y+c*z=1);
2 2 2
a + b + c - 1 >= 0
8: quit;
End of Lisp run after 0.31+0.09 seconds
REDFRONT normally exiting on signal 17 (SIGCHLD)
