formulas(hints).

% 72 hints from 3 proof(s) in file easy.out, Fri Apr 13 08:53:42 2007

f(f(x,x),f(x,x)) = x # label(Sheffer_1) # label(goal) # label(1).
f(f(x,y),f(x,f(y,z))) = x # label(2).
f(x,f(y,f(x',z))) = f(x,y') # label(3).
x' = f(x,x) # label(4).
f(x,x) = x' # label(5).
f(f(c1,c1),f(c1,c1)) != c1 # label(Sheffer_1) # answer(Sheffer_1) # label(6).
c1'' != c1 # answer(Sheffer_1) # label(7).
f(f(x,y),f(x,y')) = x # label(8).
f(x',f(x,x')) = x # label(9).
f(x,f(y,x)) = f(x,y') # label(10).
x'' = x # label(11).
$F # answer(Sheffer_1) # label(12).
f(x,f(y,f(y,y))) = f(x,x) # label(Sheffer_2) # label(goal) # label(13).
f(x,y) = f(y,x) # label(14).
f(c2,f(c3,f(c3,c3))) != f(c2,c2) # label(Sheffer_2) # answer(Sheffer_2) # label(15).
f(c2,f(c3,c3')) != c2' # answer(Sheffer_2) # label(16).
f(f(x,y),f(y,f(x,z))) = y # label(17).
f(f(x,y),f(x,f(z,y))) = x # label(18).
f(x',f(x,y)) = x # label(19).
f(x',f(y,x)) = x # label(20).
f(x,f(x,y)') = f(x,y) # label(21).
f(x,f(y,x)') = f(y,x) # label(22).
f(x,f(x,y)) = f(x,y') # label(23).
f(f(x,y),f(x,y)') = f(x',f(x,y)') # label(24).
f(x',f(y,x)') = f(y',f(y,x)') # label(25).
f(x',f(x,y)') = f(x,x') # label(26).
f(x',f(y,x)') = f(x,x') # label(27).
f(x,x') = f(y,y') # label(28).
f(x,f(y,y')) = x' # label(29).
f(f(f(x,x),y),f(f(z,z),y)) = f(f(y,f(x,z)),f(y,f(x,z))) # label(Sheffer_3) # label(goal) # label(30).
f(f(f(c4,c4),c5),f(f(c6,c6),c5)) != f(f(c5,f(c4,c6)),f(c5,f(c4,c6))) # label(Sheffer_3) # answer(Sheffer_3) # label(31).
f(f(c5,c4'),f(c5,c6')) != f(c5,f(c4,c6))' # answer(Sheffer_3) # label(32).
f(f(x,y),f(f(y,z),x)) = x # label(33).
f(x,f(f(x,y),f(f(x,f(y,z)),u))) = f(x,y) # label(34).
f(x,f(y,f(z,x'))) = f(x,y') # label(35).
f(x,f(f(x',y),z)) = f(x,z') # label(36).
f(x,f(x',y)') = f(x,x') # label(37).
f(f(x,y),f(f(x,z),y)) = y # label(38).
f(f(x,y),f(y,x')) = y # label(39).
f(f(f(x,y),z),f(z,y)) = z # label(40).
f(x',f(y,f(x,z))) = f(x',y') # label(41).
f(f(x,y),f(f(z,y),x)) = x # label(42).
f(x,f(f(x,y),f(y,z))) = f(x,y) # label(43).
f(x,f(f(x,f(y,z)),f(f(x,z),u))) = f(x,f(y,z)) # label(44).
f(f(x,f(y,z)),f(z,x)) = x # label(45).
f(f(x,y),f(f(y,x'),f(y,z))) = f(y,x') # label(46).
f(f(x,y'),f(x,f(f(x,y),z))) = x # label(47).
f(f(x,y'),f(x,f(z,f(x,y)))) = x # label(48).
f(x',f(f(x,y),z)) = f(x',z') # label(49).
f(f(x,y)',f(f(x,z),y)) = f(y,f(x,z)') # label(50).
f(x,f(f(y,x'),z)') = f(x,z) # label(51).
f(f(f(x,y),z),f(z,y)') = f(z,f(x,y)') # label(52).
f(f(x,f(y,z')),f(f(y,z),x)) = x # label(53).
f(x,f(f(x',y)',z)) = x' # label(54).
f(x',f(f(x,y)',z)) = x # label(55).
f(x',f(f(y,x)',z)) = x # label(56).
f(x',f(y,f(z,x)')) = x # label(57).
f(x,f(y,f(z,x)')') = f(y,f(z,x)') # label(58).
f(f(x,y),f(y,z)') = f(x',f(y,z)') # label(59).
f(f(x,y)',f(z,y)') = f(z,f(x,y)') # label(60).
f(f(x,y)',f(z,y)) = f(f(x,y)',z') # label(61).
f(f(x,y)',f(x,z)') = f(f(x,y)',z) # label(62).
f(f(x,y)',z) = f(y,f(x,z)') # label(63).
f(x,f(y,z)') = f(y,f(x,z)') # label(64).
f(x',f(f(y,x),z)') = f(x',z) # label(65).
f(f(x,y),f(z,f(x,y'))') = f(z,x') # label(66).
f(x,f(y,f(x,z)')) = f(x,f(y,z)) # label(67).
f(x,f(f(x,y),z)) = f(x,f(y',z)) # label(68).
f(x,f(y,f(z,f(f(x,y),u))')) = f(x,f(z,y)) # label(69).
f(x,f(y,f(x,z))) = f(x,f(y,z')) # label(70).
f(f(x,y'),f(x,f(y,z))) = f(x,f(y,z))' # label(71).
f(f(x,y'),f(x,z)) = f(x,f(y,z'))' # label(72).
end_of_list.