% name: bz_1
% exist: 0
% type: Nonproductive

premises

point PO1
point PO2
point PO3
zero PO1
plus PO2 PO1 PO3

conclusions

eq_point PO2 PO3

% name: bz_2
% exist: 0
% type: Nonproductive

premises

point PO1
point PO2
point PO3
point PO4
point PO5
point PO6
plus PO1 PO2 PO3
succ PO4 PO2
plus PO1 PO4 PO5
succ PO5 PO6

conclusions

eq_point PO3 PO6

% name: bz_7
% exist: 0
% type: Nonproductive

premises

point PO1
point PO2
point PO3
zero PO1
const_x PO2
plus PO1 PO2 PO3

conclusions

eq_point PO2 PO3

% name: ax_g1
% exist: 0
% type: Branching nonproductive

premises

point PO1
point PO2

conclusions

eq_point PO1 PO2
|
~eq_point PO1 PO2

% name: bz_4
% exist: 1
% type: Productive

premises

point PO1

conclusions

point PO2
succ PO1 PO2

% name: bz_5
% exist: 1
% type: Productive

premises

point PO1
point PO2

conclusions

point PO3
plus PO1 PO2 PO3

% name: bz_3
% exist: 1
% type: Superproductive

premises


conclusions

point PO1
zero PO1

% name: bz_6
% exist: 1
% type: Superproductive

premises


conclusions

point PO1
const_x PO1

% name: bz_8
% exist: 1
% type: Superproductive

premises


conclusions

point PO1
const_y PO1

