% The LADR formulas contain function or predicate symbols
% that are not legal TPTP symbols, and we have replaced those
% symbols with new symbols.  Here is the list of the unaccepted
% symbols and the corresponding replacements.
%
%   (arity 3)        R    tptp0
%   (arity 2)        K    tptp1
%   (arity 1)        '    tptp2
%   (arity 2)        *    tptp3
%   (arity 0)        1    tptp4
%   (arity 0)        D    tptp5
%   (arity 0)        0    tptp6
%   (arity 0)        C    tptp7
%   (arity 0)        B    tptp8
%   (arity 0)        A    tptp9

cnf(sos,axiom,( tptp3(tptp4,A) = A )).
cnf(sos,axiom,( tptp3(A,tptp4) = A )).
cnf(sos,axiom,( tptp3(A,tptp2(A)) = tptp4 )).
cnf(sos,axiom,( tptp3(tptp2(A),A) = tptp4 )).
cnf(sos,axiom,( tptp3(tptp2(A),tptp3(A,B)) = B )).
cnf(sos,axiom,( tptp3(tptp3(A,B),tptp2(B)) = A )).
cnf(sos,axiom,( tptp2(tptp3(A,B)) = tptp3(tptp2(B),tptp2(A)) )).
cnf(sos,axiom,( tptp3(tptp3(A,A),B) = tptp3(A,tptp3(A,B)) )).
cnf(sos,axiom,( tptp3(tptp3(A,B),B) = tptp3(A,tptp3(B,B)) )).
cnf(sos,axiom,( tptp3(A,tptp3(B,A)) = tptp3(tptp3(A,B),A) )).
cnf(sos,axiom,( tptp3(tptp3(tptp3(A,B),A),C) = tptp3(A,tptp3(B,tptp3(A,C))) )).
cnf(sos,axiom,( tptp3(tptp3(tptp3(A,B),C),B) = tptp3(A,tptp3(B,tptp3(C,B))) )).
cnf(sos,axiom,( tptp3(tptp3(A,B),tptp3(C,A)) = tptp3(A,tptp3(tptp3(B,C),A)) )).
cnf(sos,axiom,( tptp3(tptp3(A,B),tptp3(C,A)) = tptp3(tptp3(A,tptp3(B,C)),A) )).
cnf(sos,axiom,( tptp0(A,B,C) = tptp3(tptp3(tptp3(A,B),C),tptp2(tptp3(B,C))) )).
cnf(sos,axiom,( tptp3(tptp7,A) = tptp3(A,tptp7) )).
cnf(sos,axiom,( tptp0(tptp7,tptp9,tptp8) = tptp5 )).
cnf(sos,axiom,( tptp3(A,B) = tptp3(tptp3(B,A),tptp1(A,B)) )).
cnf(sos,axiom,( tptp3(tptp3(A,B),C) = tptp3(tptp3(A,tptp3(B,C)),a(A,B,C)) )).
cnf(sos,axiom,( tptp3(tptp0(tptp7,cx,cy),cz) != tptp3(cz,tptp0(tptp7,cx,cy)) )).
cnf(sos,axiom,( tptp3(tptp3(tptp3(tptp3(tptp7,d1),d2),tptp3(tptp2(d2),tptp2(d1))),d3) != tptp3(d3,tptp3(tptp3(tptp3(tptp7,d1),d2),tptp3(tptp2(d2),tptp2(d1)))) )).
cnf(sos,axiom,( tptp3(tptp5,d) != tptp3(d,tptp5) )).
cnf(sos,axiom,( tptp1(tptp0(tptp7,d1,d2),d3) != tptp4 )).
cnf(sos,axiom,( a(d1,tptp7,tptp1(d2,d3)) != tptp4 )).
cnf(sos,axiom,( tptp0(tptp0(tptp0(tptp5,cx,cy),cx,cy),cx,cy) != tptp5 )).
cnf(sos,axiom,( tptp0(tptp3(cu,cv),tptp5,cy) != tptp3(tptp0(cu,tptp5,cy),tptp0(cv,tptp5,cy)) )).
cnf(sos,axiom,( tptp0(tptp3(cu,cv),cy,tptp5) != tptp3(tptp0(cu,cy,tptp5),tptp0(cv,cy,tptp5)) )).
cnf(sos,axiom,( tptp3(A,tptp3(A,A)) = tptp4 )).
cnf(sos,axiom,( tptp3(tptp3(A,A),A) = tptp4 )).
