% end_of_list より下にある % の一つを消して(既に一番上の % を消してある)
% filter.rb joho7.txt
% とすると otter への入力 file が得られる。また, pipe を使って下記のようにしてもよい。
% filter.rb joho7.txt | otter
% 1040 などのように等式が書かれていない所は補わなければならない。
% 0, 1 の代わりに Org, Stand が用いられている。
set(auto).
set(output_sequent).
op(300,fy,-).
formula_list(usable).
% 0 変数関数 Org; 1 変数関数 -, abs, nor, regtrig; 2 変数関数 +, *;
% 2 変数述語 =
1: all x y z ( (x + y) + z = x + y + z ) .
2: all x y ( x + y = y + x ) . 
3: all x ( x + Org = x ) . 
4: all x ( x + (-x) = Org ) . 
5: all x ( abs(-x) = abs(x) ) . 
6: all x ( abs(Org) = Org ) .
7: all x y ( abs(abs(x)+abs(y)) = abs(x)+abs(y) ).
8: all x ( abs(regtrig(x)) = abs(x) ) . 
9: all x ( abs(regtrig(x)+ -x) = abs(x) ). 
10: all x y ( abs(x * y) = abs(x) * abs(y) ). 
11: all x ( abs(nor(x)) = Stand ) . 
12: all x ( x * Stand = x ) . 
13: all x y z ( y * x + z * x = (y + z) * x ).
14: all x ( x = abs(x)*nor(x) ). 
1015: d = regtrig(b+ -a)+a . 
1016: e = abs(c+ -b)*nor(b+ -d) +b. 
1017: f = abs(e+ -d)*nor(a+ -d)+d . 
1020: abs(f+ -a) = abs(c+ -b) . 
% --------------------------------------------------------------
1030: abs(d+ -a) = abs(b+ -a) . 
1040: 
1050: abs(e+ -b) = abs(c+ -b). 
1060: 
1070: abs(e+ -d) = abs(b+ -d)+abs(c+ -b) .
1080: abs(f+ -d) = abs(e+ -d) . 
3010: 
3020: 
3030: abs(abs(d+ -e)+ -abs(d+ -a)) = abs(d+ -e)+ -abs(d+ -a).
end_of_list.
 1-4 8 1015 => 1030
% 1-5 9 1015 => 1040
% 1-4 6 7 10-12 1016 => 1050
% 1-4 14 13 1016 => 1060
% 2 7 10-12 1060 => 1070
% 1-4 6 7 10-12 1017 => 1080
% 1-4 14 13 1017 => 3010
% 10-13 3010 => 3020
% 1-7 1030 1040 1070 => 3030
% 1-5 1030 1040 1070 3020 3030 => 1020