%/*
exists(X,f(X)) and exists(X,g(X)).

goal ~ (all(X,(f(X) => h(X)) and all(X,g(X)=>j(X)))
     == all(X,all(Y,f(X) and g(Y) => h(X) and j(Y)))).

%*/
/*
prove(exists(x,f(x)) and exists(x,g(x)) =>
   all(x,(f(x) => h(x)) and all(x,g(x)=>j(x)))
   <=> all(x,all(y,f(x) and g(y) => h(x) and j(y)))).
*/


/*
f('s$1').
g('s$2').

f(_643),f(_664),g(_665) -> h(_643),h(_664).
f(_643),f(_664),g(_665) -> h(_643),j(_665).
f(_643) -> h(_643),f('s$40'),g('s$41').
f(_643),j('s$41') -> h(_643),f('s$40').
f(_643),h('s$40') -> h(_643),g('s$42').
f(_643),h('s$40'),j('s$42') -> h(_643).
g(_852),f(_873),g(_874) -> j(_852),h(_873).
g(_852),f(_873),g(_874) -> j(_852),j(_874).
g(_852) -> j(_852),f('s$43'),g('s$44').
g(_852),j('s$44') -> j(_852),f('s$43').
g(_852),h('s$43') -> j(_852),g('s$45').
g(_852),h('s$43'),j('s$45') -> j(_852).
f(_1102),g(_1103) -> h(_1102),f('s$46').
f(_1102),g(_1103) -> h(_1102),g('s$47').
f(_1102),g(_1103),h('s$46'),j('s$47') -> h(_1102).
f(_1102),g(_1103) -> j(_1103),f('s$48').
f(_1102),g(_1103) -> j(_1103),g('s$49').
f(_1102),g(_1103),h('s$48'),j('s$49') -> j(_1103).
f('s$50'),f('s$51'),g('s$53').
j('s$53') -> f('s$50'),f('s$51').
h('s$51') -> f('s$50'),g('s$54').
h('s$51'),j('s$54') -> f('s$50').
g('s$52'),f('s$51'),g('s$55').
j('s$55') -> g('s$52'),f('s$51').
h('s$51') -> g('s$52'),g('s$56').
h('s$51'),j('s$56') -> g('s$52').
h('s$50'),j('s$52') -> f('s$51'),g('s$57').
h('s$50'),j('s$52'),j('s$57') -> f('s$51').
h('s$51'),h('s$50'),j('s$52') -> g('s$58').
h('s$51'),h('s$50'),j('s$52'),j('s$58') -> [].

*/



/*
f('s1').
g('s2').

f(_643),f(_664),g(_665) -> h(_643),h(_664).
f(_643),f(_664),g(_665) -> h(_643),j(_665).
f(_643) -> h(_643),f('s40'),g('s41').
f(_643),j('s41') -> h(_643),f('s40').
f(_643),h('s40') -> h(_643),g('s42').
f(_643),h('s40'),j('s42') -> h(_643).
g(_852),f(_873),g(_874) -> j(_852),h(_873).
g(_852),f(_873),g(_874) -> j(_852),j(_874).
g(_852) -> j(_852),f('s43'),g('s44').
g(_852),j('s44') -> j(_852),f('s43').
g(_852),h('s43') -> j(_852),g('s45').
g(_852),h('s43'),j('s45') -> j(_852).
f(_1102),g(_1103) -> h(_1102),f('s46').
f(_1102),g(_1103) -> h(_1102),g('s47').
f(_1102),g(_1103),h('s46'),j('s47') -> h(_1102).
f(_1102),g(_1103) -> j(_1103),f('s48').
f(_1102),g(_1103) -> j(_1103),g('s49').
f(_1102),g(_1103),h('s48'),j('s49') -> j(_1103).
f('s50'),f('s51'),g('s53').
j('s53') -> f('s50'),f('s51').
h('s51') -> f('s50'),g('s54').
h('s51'),j('s54') -> f('s50').
g('s52'),f('s51'),g('s55').
j('s55') -> g('s52'),f('s51').
h('s51') -> g('s52'),g('s56').
h('s51'),j('s56') -> g('s52').
h('s50'),j('s52') -> f('s51'),g('s57').
h('s50'),j('s52'),j('s57') -> f('s51').
h('s51'),h('s50'),j('s52') -> g('s58').
h('s51'),h('s50'),j('s52'),j('s58') -> [].

*/