Divisions

The MIX Division: CNF theorems

input_clause(clause1,axiom,
    [++g(A,a),
     ++g(f(A),A)]).
etc, etc

input_clause(theorem,conjecture,
    [--g(A,B),
     --g(B,a)]).

The UEQ Division: Unit equality theorems

input_clause(left_inverse,axiom,
    [++equal(multiply(inverse(Y),Y,X),X)]).
etc, etc

input_clause(prove_inverse_is_self_cancelling,conjecture,
    [--equal(inverse(inverse(a)),a)]).

The SAT Division: Non-theorems

The EPR Division: CNF, effectively propositional theorems

The FOF Division: FOF theorems

input_formula(pel59_1,axiom,(
    ! [X] : 
      ( big_f(X)
    <=> ~ big_f(f(X)) )   )).

input_formula(pel59,conjecture,(
    ? [X] : 
      ( big_f(X)
      & ~ big_f(f(X)) )   )).