twee-2.3: tests/factor.p

% Axioms about arithmetic.

cnf('commutativity of +', axiom,
    X + Y = Y + X).
cnf('associativity of +', axiom,
    X + (Y + Z) = (X + Y) + Z).
cnf('commutativity of *', axiom,
    X * Y = Y * X).
cnf('associativity of *', axiom,
    X * (Y * Z) = (X * Y) * Z).
cnf('plus 0', axiom,
    '0' + X = X).
cnf('times 0', axiom,
    '0' * X = '0').
cnf('times 1', axiom,
    '1' * X = X).
cnf('distributivity', axiom,
    X * (Y + Z) = (X * Y) + (X * Z)).
cnf('minus', axiom,
    X + -X = '0').

tff(square, type, '_²' : $i > $i).
tff(cube, type, '_³' : $i > $i).
cnf(square, axiom, X² = X*X).
cnf(cube, axiom, X³ = X*(X*X)).
%cnf(two, axiom, two = '1'+'1').
%cnf(three, axiom, three = '1'+two).
%cnf(four, axiom, four = '1'+three).
%cnf(five, axiom, five = '1'+four).
%cnf(six, axiom, six = '1'+five).
%cnf(seven, axiom, seven = '1'+six).
%cnf(eight, axiom, eight = '1'+seven).
%cnf(nine, axiom, nine = '1'+eight).
%cnf(minus_six, axiom, minus_four = -four).
%cnf(minus_six, axiom, minus_six = -six).

%fof(factoring, conjecture,
%    ?[A,B,C]: ![X]:
%      X³ + ((minus_six*(X²)) + ((nine*X) + minus_four)) = ((X +
%      -'1')*((X + -'1') * (X + -four)))).

%cnf(a, conjecture, (-x)*y = -(y*x)).

fof(factoring, conjecture,
    ?[A,B,C]: ![X]:
    X³ +
    (-(('1'+('1'+('1'+('1'+('1'+'1')))))*(X²)) +
     ((('1'+('1'+('1'+('1'+('1'+('1'+('1'+('1'+'1'))))))))*X) +
     -('1'+('1'+('1'+'1'))))) =
    (X + -A)*((X + -B)*(X + -C))).