Apple Banana Pineapple puzzle

abp.py

#!/usr/bin/env python3

from z3 import *

a, b, p = Reals('a b p')
s = Solver()
s.add((a / (b + p)) + (b / (a + p)) + (p / (a + b)) == 4)
s.add(b != -p)
s.add(a != -p)
s.add(a != -b)

res = s.check()
if res == sat:
    # print one solution (many might exist)
    m = s.model()
    print('apple =', m[a])
    print('banana =', m[b])
    print('pineapple =', m[p])
else:
    # unsat means no solution found
    print(res)