The modified problem reduction format of Plaisted [87] has been implemented in C Prolog and compiled in Quintus Prolog. This complete first-order strategy is based on a sequent-style proof system which does not require contrapositives of clauses to be used. This strategy is implemented in a back chaining manner with caching of solutions to avoid repeated work on the same subgoal. The prover also permits forward chaining and term rewriting. Paramodulation is simulated by unification and term rewriting using a special representation for the input. The C Protog source code is about 35,000 bytes long and has been distributed to probably over 100 sites together with some example files. One of the main advantages of this prover is that it is compact and relatively easy to understand at a high level. This has made it possible to perform numerous experiments and test numerous modifications rapidly. This also makes the prover suitable for instructional use, The prover has been tested on a wide variety of problems and has obtained automatic proofs in set theory, combinatory logic, ternary Boolean algebra, and many other areas. We are now studying the addition of a priority mechanism to the basic depth-first iterative deepening search strategy used by the prover. This has reduced the running time of many problems, often by an order of magnitude or more.