assume [A,B,C] : (point(A) & point(B) & A != B & point(C) & cong(A,B,B,C) & cong(B,C,C,A))
disjunction (C = A | C != A)
  case (C = A)
    infer (A = B)
    lookup contradiction
  case (C != A)
    disjunction (C = B | C != B)
      case (C = B)
        infer (A = B)
        lookup contradiction
      case (C != B)
        lookup (C! = A & C != B)
    end_disjunction
  lookup (C != A & C != B)       % da li treba ovaj korak uopste?
end_disjunction
                                  % infer (C!=A & C!=B) % ovo ne treba sigurno
