def backward_chaining(kb, theorems, substs, variables, lista, lista_coeficienti = [], coef=None):
    if len(theorems) == 0:
        lista += [substs]
        if coef != None:
            print(coef)
        return True

    is_proved = False
    print("Trying to demonstrate ")
    print_formula(theorems[0])
    q_prim = substitute(theorems[0], substs)

    if q_prim == None and substs == {}:
        q_prim = theorems[0]

    print("Substituted it with: ")
    print_formula(q_prim)
    print("")
    for sentence in kb:
        substs_prim = unify(get_conclusion(sentence), q_prim)
        if substs_prim == False:
            continue
        if substs_prim != {}:
            print("Unified it into")
        new_substs = copy.deepcopy(substs)
        for (k, v) in substs_prim.items():
            print("Variable " + str(k) + " value ", end = '')
            print_formula(v)
            new_substs[k] = v
        print("")

        new_coef = None
        if coef != None:
            new_coef = coef

            minimum = 1
            for goal in get_premises(sentence):
                minimum = min(minimum, goal[3])
                new_coef *= minimum

        new_goals = get_premises(sentence) + theorems[1:]

        if new_goals != []:
            print("New theorems to be proven ")
        for goal in new_goals:
            print_formula(goal)
        print("")

        is_proved |=  backward_chaining(kb, new_goals, new_substs, variables, lista, lista_coeficienti, new_coef)

    return is_proved