fof(true_False, axiom, ~ (true1 = false1)).
fof(infix_pl_sort, axiom, ![X, X1]: (sort(int, infix_pl(X, X1)) = infix_pl(X, X1))).
fof(assoc, axiom, ![X, Y, Z]: (infix_pl(infix_pl(X, Y), Z) = infix_pl(X, infix_pl(Y, Z)))).
fof(unit_def_l, axiom, ![X]: (infix_pl(const_0, X) = X)).
fof(inv_def_l, axiom, ![X]: (infix_pl(prefix_mn(X), X) = const_0)).
fof(antisymm, axiom, ![X, Y]: (infix_lseq(X, Y) => (infix_lseq(Y, X) => (X = Y)))).
fof(compatOrderAdd, axiom, ![X, Y, Z]: (infix_lseq(X, Y) => infix_lseq(infix_pl(X, Z), infix_pl(Y, Z)))).
fof(select_eq, axiom, ![A, B]: ![M]: ![A1, A2]: ![B1]: ((A1 = A2) => (get(B, A, set(B, A, M, A1, B1), A2) = sort(B, B1)))).

fof(q_TL_deref, axiom, ![S]: ![Mint_0]: infix_lseq(prefix_mn(const_2147483648), get(int, addr, Mint_0, S))).

fof(q_foo, conjecture, $false).