This is a Critical Pairs Theorem Prover (CPTP) for automated theorem proving of equations. There is a discussion of the CPTP and a note on the history of the problem "Does t = x imply u = v?".

Choose a term t

Enter a prefix form term t, using the binary operation +, in the following.

[Example: ++y+xzy]

Enter your choice of t: = x
Or choose t from this list.

Control Parameters

The maximum length of a term in a critical pair:

5 10 15 20 25 30 35 40 45 50
The maximum number of new critical pairs to be generated:

50 100 500 1000 2000 3000 4000 5000

Output Format

	Give a complete list of derived identities.
	Give just the identities needed to prove u = v, if a proof is found.
	*****************
	Give the details of the critical pair computations (i.e., the details of the steps)!