\documentstyle[11pt]{article} \textwidth=6in \textheight=9in \hoffset=-.5in \voffset=-1in \parskip=.05in \begin{document} \title{\Large \bf An Entry in the 1992 Overbeek Theorem-Proving Contest\thanks{This work was supported by the Applied Mathematical Sciences subprogram of the Office of Energy Research, U.S. Department of Energy, under contract W-31-109-Eng-38.}} \author{{\it Ewing L. Lusk {\rm and} William W. McCune} \\ Mathematics and Computer Science Division \\ Argonne National Laboratory \\ lusk@mcs.anl.gov \\ mccune@mcs.anl.gov} \maketitle \begin{abstract} At CADE-10 Ross Overbeek proposed a contest to stimulate and reward work in automated theorem proving. This paper represents an entry, or perhaps a family of related entries, in the contest. \end{abstract} \thispagestyle{empty} \section{Introduction} The Conference on Automated Deduction (CADE) has been for nearly twenty years a meeting where both theoreticians and system implementors present their work. Feeling perhaps that the conference was becoming dominated by the theoreticians, Ross Overbeek proposed at CADE-10 in 1990 a contest to stimulate work on the implementation and use of theorem-proving systems. The challenge was to prove a set of theorems, and do so with a uniform approach. That is, it was not allowed to set parameters in the system to specialize it for individual problems. There were actually two separate contests, one represented by a set of seven problems designed to test basic inference components, and the other represented by a set of ten problems designed to test equality-based systems. This paper describes our experiences in preparing to enter the contest with Otter\cite{otter2-guide,otter22} and ROO\cite{roo-exp,roo-tm}, two systems developed at Argonne National Laboratory. ROO is a parallel version of Otter, but has such different behavior in some cases that we treat them a separate entries. We entered each of them in both contests. Some of the problems are difficult ones, and although many of the problems had been done before with Otter, in each case we had set Otter's many input parameters in a way customized to the problem at hand, and chosen a set of support that appeared to us to be most natural. It was a challenge to come up with a uniform set of parameter settings and a uniform algorithm for picking the set of support that would allow Otter to prove each of the theorems. \section{Results} Otter and ROO proved all seven theorems in the basic set first five of the ten problems in the equality set. See Section \ref{settings} for the options settings and set of suport used. Tables 1 and 2 list the results on the two sets for Otter, for ROO running with 8 processors, and for ROO with 12 processors. The Otter jobs were run on SPARCstation 2. We used Otter 2.2, the version that was released in July 1991. The ROO jobs were run on an Alliant 2800 with 12 (Intel i860) processors. The version of ROO we used is based on Otter 2.2xa+ (June 1992). \begin{table}[htbp] \centering \begin{tabular}{lrrr} & Otter & ROO-8 & ROO-12 \\ \hline \multicolumn{4}{c}{Theorem 1: $x^2=e$ Group} \\ proof time & 0.20 & 0.32 & 0.32 \\ generated & 222 & 2300 & 1867 \\ kept & 13 & 30 & 40 \\ memory (K) & 31 & 728 & 564 \\ \hline \multicolumn{4}{c}{Theorem 2: Commutator} \\ proof time & 35.60 & 26.89 & 25.97 \\ generated & 20575 & 88838 & 131429 \\ kept & 4505 & 3684 & 1697 \\ memory (K) & 1564 & 12515 & 12670 \\ \hline \multicolumn{4}{c}{Theorem 3: $x^2=x$ Ring} \\ proof time & 145.41 & 35.57 & 38.18 \\ generated & 56025 & 134744 & 221890 \\ kept & 13990 & 4316 & 2736 \\ memory (K) & 4342 & 14333 & 18739 \\ \hline \multicolumn{4}{c}{Theorem 4: XGK} \\ proof time & 407.50 & 159.87 & 55.37 \\ generated & 177109 & 663722 & 263233 \\ kept & 15320 & 16519 & 9466 \\ memory (K) & 8047 & 19539 & 22189 \\ \hline \multicolumn{4}{c}{Theorem 5: Imp-4 (CD-67)} \\ proof time & 7711.98 & 1051.55 & 909.95 \\ generated & 8341570 & 7171447 & 8182376 \\ kept & 17862 & 14855 & 17666 \\ memory (K) & 10729 & 13983 & 15098 \\ \hline \multicolumn{4}{c}{Theorem 6: MV-1 (CD-57)} \\ proof time & 17.68 & 4.37 & 14.71 \\ generated & 16687 & 24159 & 114051 \\ kept & 4837 & 1024 & 2000 \\ memory (K) & 2171 & 6479 & 12161 \\ \hline \multicolumn{4}{c}{Theorem 7: MV-2 (CD-60)} \\ proof time & 2184.96 & 427.89 & 152.53 \\ generated & 3214280 & 4311090 & 1997084 \\ kept & 16250 & 12374 & 10750 \\ memory (K) & 7216 & 13664 & 13755 \\ \end{tabular} \caption{Results for Basic Theorems} \end{table} \begin{table}[htbp] \centering \begin{tabular}{lrrr} & Otter & ROO-8 & ROO-12 \\ \hline \multicolumn{4}{c}{Theorem EQ-1: Commutator} \\ proof time & 1.49 & 0.76 & 0.86 \\ generated & 542 & 1727 & 2144 \\ kept & 114 & 91 & 89 \\ memory (K) & 255 & 1208 & 1460 \\ % \hline % \multicolumn{4}{c}{Theorem EQ-1: Commutator, SOS=everything} \\ % proof time & 1.51 & 0.46 & 1.31 \\ % generated & 554 & 1280 & 4570 \\ % kept & 115 & 74 & 128 \\ % memory (K) & 255 & 952 & 2356 \\ \hline \multicolumn{4}{c}{Theorem EQ-2: Robbins, $c+c=c$} \\ proof time & 98.19 & 18.63 & 13.43 \\ generated & 50001 & 56067 & 59151 \\ kept & 4548 & 2450 & 1235 \\ memory (K) & 5652 & 12676 & 13342 \\ % \hline % \multicolumn{4}{c}{Theorem EQ-2: Robbins, SOS=everything} \\ % proof time & 243.35 & 30.84 & 18.82 \\ % generated & 93380 & 45704 & 55703 \\ % kept & 4467 & 2494 & 1486 \\ % memory (K) & 6067 & 15420 & 13277 \\ \hline \multicolumn{4}{c}{Theorem EQ-3: TBA} \\ proof time & 16.78 & 4.10 & 3.16 \\ generated & 3945 & 9307 & 11170 \\ kept & 1030 & 620 & 378 \\ memory (K) & 1564 & 4880 & 5043 \\ \hline \multicolumn{4}{c}{Theorem EQ-4: Group single axiom} \\ proof time & 44.12 & 10.56 & 9.25 \\ generated & 3417 & 11778 & 16118 \\ kept & 2507 & 1015 & 863 \\ memory (K) & 4470 & 13889 & 17110 \\ \hline \multicolumn{4}{c}{Theorem EQ-5: Wajsberg algebra} \\ proof time & 2248.86 & 425.99 & 491.67 \\ generated & 1012625 & 971543 & 1437272 \\ kept & 5897 & 4374 & 4022 \\ memory (K) & 6801 & 13376 & 14525 \\ \end{tabular} \caption{Results for Equality Problems} \end{table} \section{Settings and Set of Support} \label{settings} Within each set, all of the Otter jobs used the same settings. However, the settings for the basic set were substantially different from those for the equality set. The ROO jobs used settings slightly different from the Otter jobs, and (for small technical reasons) the ROO settings for the basic set varied slightly, depending on whether equality is present. For the basic set, the initial set of support consisted of the positive input clauses, except (x=x). For the equality set, the initial set of support depended on whether the theorem has an obvious special hypothesis---if so, then the set of support was the special hypothesis and the denial of the conclusion; if not, the set of support consisted of all input clauses. The rules for the equality set state that an ordering on the symbols may be input along with the input clauses. The ordering is used to orient equality literals. \subsection{Settings for the Basic Set} {\small \begin{center} \begin{tabular}{lll} Otter: baisc set & ROO: basic with equality & ROO: basic without equality \\ \hline & set(index\_for\_back\_demod) & \\ set(hyper\_res) & set(hyper\_res) &set(hyper\_res) \\ set(back\_demod) & set(back\_demod) & \\ set(dynamic\_demod\_all) & set(dynamic\_demod\_all) & \\ assign(pick\_given\_ratio,5)&assign(pick\_given\_ratio,5)&assign(pick\_given\_ratio,5)\\ clear(print\_kept) & clear(print\_kept) & clear(print\_kept) \\ assign(max\_mem,20000) & assign(max\_mem,32000) & assign(max\_mem,32000) \\ set(control\_memory) & set(control\_memory) & set(control\_memory)\\ \hline \end{tabular} \end{center} } \subsection{Settings for the Equality Set} {\small \begin{center} \begin{tabular}{lll} Otter: equality set & ROO: equality set \\ \hline set(knuth\_bendix) & set(knuth\_bendix) \\ set(index\_for\_back\_demod) & set(index\_for\_back\_demod) \\ set(process\_input) & set(process\_input) \\ assign(max\_mem,16000) & assign(max\_mem,32000) \\ set(control\_memory) & set(control\_memory) \\ set(lex\_rpo) & set(lex\_rpo) \\ clear(print\_kept) & clear(print\_kept) \\ clear(print\_new\_demod) & clear(print\_new\_demod) \\ clear(print\_back\_demod) & clear(print\_back\_demod) \\ \hline \end{tabular} \end{center} } \subsection{Description of the Settings} \begin{description} \item[set(hyper\_res).] This option activates the inference rule hyperresolution. \item[set(back\_demod).] When new equalities are deduced, use them as rewrite rules. \item[set(dynamic\_demod\_all).] Use all new orientable equalities as rewrite rules. \item[set(index\_for\_back\_demod).] This options causes indexing to be used when searching for terms to which a new rewrite rule can be applied. ROO requires this ``option'' whenever back demodulation is enabled. Otter frequently benefits from this option. \item[assign(pick\_given\_ratio,5).] By default Otter chooses each new given clause based on its symbol count. This means that a heavy clause that is needed for the proof cannot be used until all lighter clauses have been used. Recently we have found it useful to mix this strategy with a breadth-first strategy by choosing some percentage of the given clauses according to the order in which they are generated rather than by weight. This setting chooses every sixth given clause in order of generation, and the rest by symbol count. \item[clear(print\_kept). clear(print\_new\_demod).clear(print\_back\_demod).] These options suppress output, saving file space and a little time. \item[assign(max\_mem,20000).] This setting restricts memory usage to 20 Megabytes. Its real use is in conjunction with the next parameter. \item[set(control\_memory).] This setting has a relatively complex effect. Every ten given clauses, memory usage is analyzed. If more than a third of {\tt max\_mem} has been used, then the {\tt max\_weight} parameter is automatically set to a value calculated such that only the lightest 5\% of the clauses in the current set of support have lower weight. No clauses are deleted, but from this point on, new clauses heavier than this weight are discarded. Using this parameter has the effect of allowing the system to choose a value for {\tt max\_weight} and adjust it during the run. \item[set(knuth\_bendix).] This option causes Otter and ROO to automatically set a collection of options that approximate a Knuth-Bendix completion procedure. Under this option, the theorem prover orders equalities, paramodulates from left sides into left sides, and back demodulates. \item[set(process\_input).] This option causes all input clauses to be processed (subsumption, demodulation, equality ordering, back demodulation) as if they were generated clauses. \item[lex({\it list of symbols}).] This command specifies an ordering on constant, function, and predicate symbols, with smallest first. For the experiments described in this paper, the ordering is used to attempt to orient equalities. \item[set(lex\_rpo).] This options specifies the lexicographic recursive path ordering for comparing terms when attempting to orient equalities. \item[lrpo\_lr\_status({\it list of symbols}).] This command specifies that function symbols are to be compared left-to-right when applying the lexicographic recursive path ordering. \end{description} \section{Failures on Equality Theorems 6--10} \begin{description} \item[Theorem EQ-6.] {\it The fragment \{B,W,M\} of combinatory logic contains fixed point combinators.} Otter found a proof, but the setting were different from those used in theorems EQ-1 through EQ-5. The important difference is that the initial set of support consists of the denial only (so that all generated clauses are negative), and paramodulation is allowed into both arguments of equality literals. The following input file causes Otter to find a proof of EQ-6 in about 27 seconds. {\small \begin{verbatim} set(para_into). clear(para_from_right). set(order_eq). assign(max_mem, 16000). set(lex_rpo). clear(print_kept). lex([B,W,L,M,a(x,x),f(x)]). lrpo_lr_status([a(x,x)]). list(usable). (x = x). (a(a(a(B,x),y),z) = a(x,a(y,z))). (a(a(W,x),y) = a(a(x,y),y)). (a(M,x) = a(x,x)). end_of_list. list(sos). (a(y,f(y)) != a(f(y),a(y,f(y)))) | $Ans(y). end_of_list. list(demodulators). (a(a(a(B,x),y),z) = a(x,a(y,z))). end_of_list. \end{verbatim} } \item[Theorem EQ-7.] {\it Rings in which $x^3=x$ are commutative.} As far as we know, Otter has never found a proof of this theorem, except with highly specialized settings and weight templates. We suspect that with associative-commutative unification, Otter would be able to prove it. \item[Theorem EQ-8.] {\it The fragment \{B,W\} of combinatory logic contains fixed point combinators.} This theorem is much more difficult than EQ-6, and the strategy above that works for EQ-6 fails for EQ-8. The kernel method \cite{presence-absence}, which was developed for this type of problem, finds a proof of EQ-8 within a few seconds. \item[Theorems EQ-9 and EQ-10.] On Moufang identities in nonassociative rings (EQ-9), and on right alternative nonassociative rings (EQ-10). The complicated definitions in these theorems cause terms in the conclusion to be greatly expanded. Otter cannot cope with the complex conclusions, because it likes to focus on simple terms. WWE also believe that associative-commutative unification would be helpful for these theorems. \end{description} \section{Summary of Otter Outputs for the Basic Set} \subsection{Theorem 1: $x^2=e$ Groups are Commutative (P-form)} {\small \begin{verbatim} ----- OTTER 2.2, July 1991 ----- The job began on altair.mcs.anl.gov, Wed Jun 3 13:15:19 1992 The command was "otter22". set(hyper_res). set(back_demod). set(dynamic_demod_all). assign(pick_given_ratio,5). clear(print_kept). assign(max_mem,20000). set(control_memory). list(usable). 1 [] -P(x,y,u) | -P(y,z,v) | -P(u,z,w) | P(x,v,w). 2 [] -P(x,y,u) | -P(y,z,v) | -P(x,v,w) | P(u,z,w). 3 [] -P(x,y,u) | -P(x,y,v) | eq(u,v). 4 [] eq(x,x). 5 [] -eq(x,y) | eq(y,x). 6 [] -eq(x,y) | -eq(y,z) | eq(x,z). 7 [] -eq(u,v) | -P(u,x,y) | P(v,x,y). 8 [] -eq(u,v) | -P(x,u,y) | P(x,v,y). 9 [] -eq(u,v) | -P(x,y,u) | P(x,y,v). 10 [] -eq(u,v) | eq(f(u,x),f(v,x)). 11 [] -eq(u,v) | eq(f(x,u),f(x,v)). 12 [] -eq(u,v) | eq(g(u),g(v)). end_of_list. list(sos). 13 [] P(e,x,x). 14 [] P(x,e,x). 15 [] P(g(x),x,e). 16 [] P(x,g(x),e). 17 [] P(x,y,f(x,y)). 18 [] P(x,x,e). 19 [] P(a,b,c). 20 [] -P(b,a,c). end_of_list. OTTER sets dynamic_demod, because back_demod is set. OTTER sets order_eq, because dynamic_demod is set. ----> UNIT CONFLICT at 0.20 sec ----> 35 [binary,34,20] . Level of proof is 3, length is 4. ---------------- PROOF ---------------- 1 [] -P(x,y,u) | -P(y,z,v) | -P(u,z,w) | P(x,v,w). 2 [] -P(x,y,u) | -P(y,z,v) | -P(x,v,w) | P(u,z,w). 13 [] P(e,x,x). 14 [] P(x,e,x). 18 [] P(x,x,e). 19 [] P(a,b,c). 20 [] -P(b,a,c). 21 [hyper,19,2,18,14] P(c,b,a). 22 [hyper,19,1,18,13] P(a,c,b). 23 [hyper,21,1,18,13] P(c,a,b). 34 [hyper,23,2,22,19] P(b,a,c). 35 [binary,34,20] . ------------ end of proof ------------- -------------- statistics ------------- clauses input 20 clauses given 9 clauses generated 222 demod & eval rewrites 26 tautologies deleted 0 clauses forward subsumed 209 (subsumed by sos) 13 clauses kept 13 new demodulators 1 empty clauses 1 clauses back demodulated 0 clauses back subsumed 0 sos size 12 Kbytes malloced 31 ----------- times (seconds) ----------- run time 0.22 (run time 0 hr, 0 min, 0 sec) system time 0.11 input time 0.02 clausify time 0.00 hyper_res time 0.05 pre_process time 0.09 demod time 0.01 weigh cl time 0.00 for_sub time 0.05 renumber time 0.00 keep cl time 0.00 print_cl time 0.00 conflict time 0.00 post_process time 0.01 back demod time 0.00 back_sub time 0.01 lex_rpo time 0.00 The job finished Wed Jun 3 13:15:19 1992 \end{verbatim} } \subsection{Theorem 2: The Commutator Theorem (P-form)} {\small \begin{verbatim} ----- OTTER 2.2, July 1991 ----- The job began on altair.mcs.anl.gov, Wed Jun 3 13:13:02 1992 The command was "otter22". set(hyper_res). set(back_demod). set(dynamic_demod_all). assign(pick_given_ratio,5). clear(print_kept). assign(max_mem,20000). set(control_memory). list(usable). 1 [] -P(x,y,u) | -P(y,z,v) | -P(u,z,w) | P(x,v,w). 2 [] -P(x,y,u) | -P(y,z,v) | -P(x,v,w) | P(u,z,w). 3 [] -P(x,y,u) | -P(x,y,v) | eq(u,v). 4 [] eq(x,x). 5 [] -eq(x,y) | eq(y,x). 6 [] -eq(x,y) | -eq(y,z) | eq(x,z). 7 [] -eq(u,v) | -P(u,x,y) | P(v,x,y). 8 [] -eq(u,v) | -P(x,u,y) | P(x,v,y). 9 [] -eq(u,v) | -P(x,y,u) | P(x,y,v). 10 [] -eq(u,v) | eq(f(u,x),f(v,x)). 11 [] -eq(u,v) | eq(f(x,u),f(x,v)). 12 [] -eq(u,v) | eq(g(u),g(v)). 13 [] -P(x,x,y) | P(x,y,e). 14 [] -P(x,x,y) | P(y,x,e). end_of_list. list(sos). 15 [] P(e,x,x). 16 [] P(x,e,x). 17 [] P(g(x),x,e). 18 [] P(x,g(x),e). 19 [] P(x,y,f(x,y)). 20 [] P(a,b,c). 21 [] P(c,g(a),d). 22 [] P(d,g(b),h). 23 [] P(h,b,j). 24 [] P(j,g(h),k). 25 [] -P(k,g(b),e). end_of_list. OTTER sets dynamic_demod, because back_demod is set. OTTER sets order_eq, because dynamic_demod is set. ----> UNIT CONFLICT at 35.60 sec ----> 4648 [binary,4647,49] . Level of proof is 15, length is 37. ---------------- PROOF ---------------- 1 [] -P(x,y,u) | -P(y,z,v) | -P(u,z,w) | P(x,v,w). 2 [] -P(x,y,u) | -P(y,z,v) | -P(x,v,w) | P(u,z,w). 3 [] -P(x,y,u) | -P(x,y,v) | eq(u,v). 9 [] -eq(u,v) | -P(x,y,u) | P(x,y,v). 13 [] -P(x,x,y) | P(x,y,e). 14 [] -P(x,x,y) | P(y,x,e). 15 [] P(e,x,x). 16 [] P(x,e,x). 17 [] P(g(x),x,e). 18 [] P(x,g(x),e). 19 [] P(x,y,f(x,y)). 20 [] P(a,b,c). 21 [] P(c,g(a),d). 22 [] P(d,g(b),h). 23 [] P(h,b,j). 24 [] P(j,g(h),k). 25 [] -P(k,g(b),e). 28 [hyper,17,2,17,16] P(e,x,g(g(x))). 37 [hyper,21,2,17,16] P(d,a,c). 39 [hyper,37,1,17,15] P(g(d),c,a). 41 [hyper,22,2,17,16] P(h,b,d). 45,44 [hyper,41,3,23] eq(j,d). 46 [hyper,41,1,17,15] P(g(h),d,b). 47 [back_demod,24,demod,45] P(d,g(h),k). 48 [hyper,19,14] P(f(x,x),x,e). 49 [hyper,19,13] P(x,f(x,x),e). 65,64 [hyper,19,3,16] eq(f(x,e),x). 67,66 [hyper,19,3,15] eq(f(e,x),x). 79 [hyper,19,2,19,19] P(f(x,y),z,f(x,f(y,z))). 80 [hyper,19,2,19,18,demod,65] P(f(x,y),g(y),x). 160 [hyper,39,2,18,19,demod,65] P(a,g(c),g(d)). 176 [hyper,46,2,18,19,demod,65] P(b,g(d),g(h)). 183,182 [hyper,28,3,19,demod,67] eq(g(g(x)),x). 192 [hyper,47,2,18,19,demod,183,65] P(k,h,d). 312 [hyper,48,1,20,19,demod,67] P(f(a,a),c,b). 317,316 [hyper,49,3,19] eq(f(x,f(x,x)),e). 319 [hyper,49,2,192,19,demod,65] P(d,f(h,h),k). 497 [hyper,176,3,19] eq(f(b,g(d)),g(h)). 705 [hyper,312,1,19,19] P(a,f(a,c),b). 715,714 [hyper,319,3,19] eq(f(d,f(h,h)),k). 932 [hyper,705,2,37,19] P(c,f(a,c),f(d,b)). 1180 [hyper,80,1,49,19,demod,67] P(x,x,g(x)). 1235,1234 [hyper,1180,3,19] eq(g(x),f(x,x)). 1256 [hyper,1180,2,19,160,demod,1235] P(f(a,c),c,f(d,d)). 1481,1480 [back_demod,497,demod,1235,1235] eq(f(b,f(d,d)),f(h,h)). 1534 [back_demod,25,demod,1235] -P(k,f(b,b),e). 1586,1585 [hyper,79,3,19] eq(f(f(x,y),z),f(x,f(y,z))). 3340,3339 [hyper,932,3,19] eq(f(c,f(a,c)),f(d,b)). 3736 [hyper,1256,2,48,19,demod,1586,3340,1586,1586,1481,715] P(e,c,f(a,k)). 3775 [hyper,3736,3,19,demod,67] eq(f(a,k),c). 3794 [hyper,3775,9,19] P(a,k,c). 3817 [hyper,3794,2,79,312,demod,317] P(e,k,b). 3959,3958 [hyper,3817,3,19,demod,67] eq(k,b). 4647 [back_demod,1534,demod,3959] -P(b,f(b,b),e). 4648 [binary,4647,49] . ------------ end of proof ------------- -------------- statistics ------------- clauses input 25 clauses given 165 clauses generated 20575 demod & eval rewrites 32696 tautologies deleted 0 clauses forward subsumed 18332 (subsumed by sos) 6484 clauses kept 4505 new demodulators 117 empty clauses 1 clauses back demodulated 2262 clauses back subsumed 60 sos size 2089 Kbytes malloced 1564 ----------- times (seconds) ----------- run time 35.65 (run time 0 hr, 0 min, 35 sec) system time 6.88 input time 0.01 clausify time 0.00 hyper_res time 6.07 pre_process time 19.21 demod time 6.33 weigh cl time 0.00 for_sub time 6.37 renumber time 0.94 keep cl time 2.18 print_cl time 0.00 conflict time 1.48 post_process time 9.71 back demod time 7.73 back_sub time 1.82 lex_rpo time 0.00 The job finished Wed Jun 3 13:13:44 1992 \end{verbatim} } \subsection{Theorem 3: $x^2=x$ Rings are Commutative (P-form)} {\small \begin{verbatim} ----- OTTER 2.2, July 1991 ----- The job began on altair.mcs.anl.gov, Wed Jun 3 13:19:36 1992 The command was "otter22". set(hyper_res). set(back_demod). set(dynamic_demod_all). assign(pick_given_ratio,5). clear(print_kept). assign(max_mem,20000). set(control_memory). list(usable). 1 [] -S(x,y,u) | -S(y,z,v) | -S(u,z,w) | S(x,v,w). 2 [] -S(x,y,u) | -S(y,z,v) | -S(x,v,w) | S(u,z,w). 3 [] -S(x,y,u) | -S(x,y,v) | eq(u,v). 4 [] eq(x,x). 5 [] -eq(x,y) | eq(y,x). 6 [] -eq(x,y) | -eq(y,z) | eq(x,z). 7 [] -eq(u,v) | -S(u,x,y) | S(v,x,y). 8 [] -eq(u,v) | -S(x,u,y) | S(x,v,y). 9 [] -eq(u,v) | -S(x,y,u) | S(x,y,v). 10 [] -eq(u,v) | eq(j(u,x),j(v,x)). 11 [] -eq(u,v) | eq(j(x,u),j(x,v)). 12 [] -eq(u,v) | eq(g(u),g(v)). 13 [] -S(x,y,z) | S(y,x,z). 14 [] -P(x,y,u) | -P(y,z,v) | -P(u,z,w) | P(x,v,w). 15 [] -P(x,y,u) | -P(y,z,v) | -P(x,v,w) | P(u,z,w). 16 [] -P(x,y,v1) | -P(x,z,v2) | -S(y,z,v3) | -P(x,v3,v4) | S(v1,v2,v4). 17 [] -P(x,y,v1) | -P(x,z,v2) | -S(y,z,v3) | -S(v1,v2,v4) | P(x,v3,v4). 18 [] -P(y,x,v1) | -P(z,x,v2) | -S(y,z,v3) | -P(v3,x,v4) | S(v1,v2,v4). 19 [] -P(y,x,v1) | -P(z,x,v2) | -S(y,z,v3) | -S(v1,v2,v4) | P(v3,x,v4). 20 [] -P(x,y,u) | -P(x,y,v) | eq(u,v). 21 [] -eq(u,v) | -P(u,x,y) | P(v,x,y). 22 [] -eq(u,v) | -P(x,u,y) | P(x,v,y). 23 [] -eq(u,v) | -P(x,y,u) | P(x,y,v). 24 [] -eq(u,v) | eq(f(u,x),f(v,x)). 25 [] -eq(u,v) | eq(f(x,u),f(x,v)). end_of_list. list(sos). 26 [] S(0,x,x). 27 [] S(x,0,x). 28 [] S(g(x),x,0). 29 [] S(x,g(x),0). 30 [] S(x,y,j(x,y)). 31 [] P(0,x,0). 32 [] P(x,0,0). 33 [] P(x,y,f(x,y)). 34 [] P(x,x,x). 35 [] P(a,b,c). 36 [] -P(b,a,c). end_of_list. OTTER sets dynamic_demod, because back_demod is set. OTTER sets order_eq, because dynamic_demod is set. ----> UNIT CONFLICT at 145.41 sec ----> 14124 [binary,14123,36] . Level of proof is 16, length is 41. ---------------- PROOF ---------------- 1 [] -S(x,y,u) | -S(y,z,v) | -S(u,z,w) | S(x,v,w). 2 [] -S(x,y,u) | -S(y,z,v) | -S(x,v,w) | S(u,z,w). 3 [] -S(x,y,u) | -S(x,y,v) | eq(u,v). 13 [] -S(x,y,z) | S(y,x,z). 14 [] -P(x,y,u) | -P(y,z,v) | -P(u,z,w) | P(x,v,w). 15 [] -P(x,y,u) | -P(y,z,v) | -P(x,v,w) | P(u,z,w). 16 [] -P(x,y,v1) | -P(x,z,v2) | -S(y,z,v3) | -P(x,v3,v4) | S(v1,v2,v4). 17 [] -P(x,y,v1) | -P(x,z,v2) | -S(y,z,v3) | -S(v1,v2,v4) | P(x,v3,v4). 18 [] -P(y,x,v1) | -P(z,x,v2) | -S(y,z,v3) | -P(v3,x,v4) | S(v1,v2,v4). 19 [] -P(y,x,v1) | -P(z,x,v2) | -S(y,z,v3) | -S(v1,v2,v4) | P(v3,x,v4). 20 [] -P(x,y,u) | -P(x,y,v) | eq(u,v). 23 [] -eq(u,v) | -P(x,y,u) | P(x,y,v). 26 [] S(0,x,x). 27 [] S(x,0,x). 28 [] S(g(x),x,0). 29 [] S(x,g(x),0). 30 [] S(x,y,j(x,y)). 31 [] P(0,x,0). 32 [] P(x,0,0). 33 [] P(x,y,f(x,y)). 34 [] P(x,x,x). 35 [] P(a,b,c). 36 [] -P(b,a,c). 37 [hyper,35,15,35,34] P(c,b,c). 38 [hyper,35,14,34,35] P(a,c,c). 43,42 [hyper,28,3,27] eq(g(0),0). 44 [hyper,28,2,28,27] S(0,x,g(g(x))). 63 [hyper,30,19,34,37,30] P(j(b,c),b,j(b,c)). 92 [hyper,30,17,38,34,30] P(a,j(c,a),j(c,a)). 120 [hyper,30,13] S(x,y,j(y,x)). 126,125 [hyper,30,3,27] eq(j(x,0),x). 128,127 [hyper,30,3,26] eq(j(0,x),x). 131 [hyper,30,2,30,28,demod,126] S(j(x,g(y)),y,x). 139 [hyper,30,1,28,30,demod,128] S(g(x),j(x,y),y). 150,149 [hyper,33,20,32] eq(f(x,0),0). 152,151 [hyper,33,20,31] eq(f(0,x),0). 193 [hyper,33,18,34,33,29,demod,152] S(x,f(g(x),x),0). 248 [hyper,33,16,34,33,29,demod,150] S(x,f(x,g(x)),0). 258 [hyper,33,16,33,34,28,demod,150] S(f(x,g(x)),x,0). 325,324 [hyper,44,3,30,demod,128] eq(g(g(x)),x). 450 [hyper,120,2,120,28,demod,128] S(j(g(x),y),x,y). 475 [hyper,120,1,28,120,demod,126] S(g(x),j(y,x),y). 1477 [hyper,139,3,30] eq(j(g(x),j(x,y)),y). 1905 [hyper,193,2,29,131,demod,43,126,325,43,126] S(0,f(x,g(x)),x). 2976 [hyper,248,3,30] eq(j(x,f(x,g(x))),0). 3558 [hyper,258,2,30,131,demod,43,126] S(j(x,f(y,g(y))),y,x). 7630,7629 [hyper,1905,3,120,demod,126] eq(f(x,g(x)),x). 7631 [hyper,1905,2,450,248,demod,43,128,43,128,7630,43,128,43,128,7630,7630] S(x,x,0). 7632 [hyper,1905,1,475,248,demod,128] S(g(x),0,x). 7636 [hyper,1905,1,258,120,demod,7630,7630] S(x,j(y,x),y). 7637 [hyper,1905,1,258,30,demod,7630,7630] S(x,j(x,y),y). 7793 [back_demod,3558,demod,7630] S(j(x,y),y,x). 7836,7835 [back_demod,2976,demod,7630] eq(j(x,x),0). 8850 [hyper,63,17,34,120,120,demod,7836] P(j(b,c),j(b,j(b,c)),0). 9362,9361 [hyper,7632,3,120,demod,128] eq(g(x),x). 10116,10115 [back_demod,1477,demod,9362] eq(j(x,j(x,y)),y). 10286 [back_demod,8850,demod,10116] P(j(b,c),c,0). 10433 [hyper,92,19,34,7793,7631] P(c,j(c,a),0). 11007 [hyper,10286,19,34,7636,120,demod,128] P(b,c,c). 11206 [hyper,11007,15,33,35] P(f(b,a),b,c). 11469 [hyper,10433,17,34,7637,120,demod,128] P(c,a,c). 12377 [hyper,11206,15,33,34] P(c,a,f(b,a)). 14119 [hyper,12377,20,11469] eq(f(b,a),c). 14123 [hyper,14119,23,33] P(b,a,c). 14124 [binary,14123,36] . ------------ end of proof ------------- -------------- statistics ------------- clauses input 36 clauses given 120 clauses generated 56025 demod & eval rewrites 77893 tautologies deleted 1 clauses forward subsumed 53529 (subsumed by sos) 19775 clauses kept 13990 new demodulators 97 empty clauses 1 clauses back demodulated 11495 clauses back subsumed 39 sos size 2410 Kbytes malloced 4342 ----------- times (seconds) ----------- run time 145.46 (run time 0 hr, 2 min, 25 sec) system time 20.87 input time 0.04 clausify time 0.00 hyper_res time 20.44 pre_process time 52.21 demod time 12.31 weigh cl time 0.00 for_sub time 18.56 renumber time 2.96 keep cl time 7.94 print_cl time 0.00 conflict time 5.10 post_process time 71.27 back demod time 63.58 back_sub time 7.18 lex_rpo time 0.00 The job finished Wed Jun 3 13:22:23 1992 \end{verbatim} } \subsection{Theorem 4: Equivalential Calculus, XGK $\rightarrow$ PYO} {\small \begin{verbatim} ----- OTTER 2.2, July 1991 ----- The job began on altair.mcs.anl.gov, Wed Jun 3 13:22:37 1992 The command was "otter22". set(hyper_res). set(back_demod). set(dynamic_demod_all). assign(pick_given_ratio,5). clear(print_kept). assign(max_mem,20000). set(control_memory). list(usable). 1 [] -P(x) | -P(e(x,y)) | P(y). end_of_list. list(sos). 2 [] P(e(x,e(e(y,e(z,x)),e(z,y)))). 3 [] -P(e(e(e(a,e(b,c)),c),e(b,a))). end_of_list. OTTER sets dynamic_demod, because back_demod is set. OTTER sets order_eq, because dynamic_demod is set. Resetting weight limit to 20. ----> UNIT CONFLICT at 407.50 sec ----> 15324 [binary,15323,3] . Level of proof is 13, length is 19. ---------------- PROOF ---------------- 1 [] -P(x) | -P(e(x,y)) | P(y). 2 [] P(e(x,e(e(y,e(z,x)),e(z,y)))). 3 [] -P(e(e(e(a,e(b,c)),c),e(b,a))). 4 [hyper,2,1,2] P(e(e(x,e(y,e(z,e(e(u,e(v,z)),e(v,u))))),e(y,x))). 6 [hyper,4,1,2] P(e(e(e(e(x,e(y,z)),e(y,x)),e(z,u)),u)). 8 [hyper,6,1,6] P(e(x,x)). 9 [hyper,6,1,4] P(e(e(x,e(e(y,e(z,x)),e(z,y))),e(u,u))). 13 [hyper,8,1,2] P(e(e(x,e(y,e(z,z))),e(y,x))). 18 [hyper,13,1,2] P(e(e(x,e(x,y)),y)). 21 [hyper,13,1,2] P(e(e(x,e(y,e(e(z,e(u,e(v,v))),e(u,z)))),e(y,x))). 39 [hyper,18,1,13] P(e(x,e(y,e(y,e(x,e(z,z)))))). 42 [hyper,18,1,2] P(e(e(x,e(y,e(e(z,e(z,u)),u))),e(y,x))). 108 [hyper,39,1,4] P(e(x,e(y,e(y,x)))). 133 [hyper,108,1,2] P(e(e(x,e(y,e(z,e(u,e(u,z))))),e(y,x))). 146 [hyper,9,1,2] P(e(e(x,e(y,e(e(z,e(e(u,e(v,z)),e(v,u))),e(w,w)))),e(y,x))). 682 [hyper,42,1,18] P(e(x,e(y,e(y,e(x,e(e(z,e(z,u)),u)))))). 2253 [hyper,133,1,2] P(e(e(e(x,e(x,y)),e(y,z)),z)). 8738 [hyper,682,1,4] P(e(x,e(y,e(e(z,e(z,y)),x)))). 8897 [hyper,8738,1,2253] P(e(e(x,e(x,y)),e(z,e(z,y)))). 9048 [hyper,8897,1,21] P(e(e(x,e(y,e(z,z))),e(u,e(u,e(y,x))))). 13855 [hyper,9048,1,4] P(e(x,e(e(y,z),e(e(z,e(y,x)),e(u,u))))). 15323 [hyper,13855,1,146] P(e(e(e(x,e(y,z)),z),e(y,x))). 15324 [binary,15323,3] . ------------ end of proof ------------- -------------- statistics ------------- clauses input 3 clauses given 587 clauses generated 177109 demod & eval rewrites 0 clauses wt,lit,sk delete 102987 tautologies deleted 0 clauses forward subsumed 58802 (subsumed by sos) 12239 clauses kept 15320 new demodulators 0 empty clauses 1 clauses back demodulated 0 clauses back subsumed 0 sos size 14735 Kbytes malloced 8047 ----------- times (seconds) ----------- run time 407.53 (run time 0 hr, 6 min, 47 sec) system time 41.90 input time 0.01 clausify time 0.00 hyper_res time 72.62 pre_process time 100.67 demod time 0.00 weigh cl time 15.72 for_sub time 18.83 renumber time 18.15 keep cl time 21.08 print_cl time 0.00 conflict time 4.38 post_process time 223.50 back demod time 0.00 back_sub time 223.01 lex_rpo time 0.00 The job finished Wed Jun 3 13:30:09 1992 \end{verbatim} } \subsection{Theorem 5: Implicational Calulus Single Axiom, CD-67 (Imp-4)} {\small \begin{verbatim} ----- OTTER 2.2, July 1991 ----- The job began on altair.mcs.anl.gov, Wed Jun 3 14:27:00 1992 The command was "otter22". set(hyper_res). set(back_demod). set(dynamic_demod_all). clear(print_kept). assign(pick_given_ratio,5). assign(max_mem,20000). set(control_memory). list(usable). 1 [] -P(x) | -P(i(x,y)) | P(y). end_of_list. list(sos). 2 [] P(i(i(i(x,y),z),i(i(z,x),i(u,x)))). 3 [] -P(i(i(a,b),i(i(b,c),i(a,c)))). end_of_list. OTTER sets dynamic_demod, because back_demod is set. OTTER sets order_eq, because dynamic_demod is set. Resetting weight limit to 20. Resetting weight limit to 18. Resetting weight limit to 16. ----> UNIT CONFLICT at 7711.98 sec ----> 17866 [binary,17865,3] . Level of proof is 40, length is 94. ---------------- PROOF ---------------- 1 [] -P(x) | -P(i(x,y)) | P(y). 2 [] P(i(i(i(x,y),z),i(i(z,x),i(u,x)))). 3 [] -P(i(i(a,b),i(i(b,c),i(a,c)))). 4 [hyper,2,1,2] P(i(i(i(i(x,y),i(z,y)),i(y,u)),i(v,i(y,u)))). 5 [hyper,4,1,4] P(i(x,i(i(y,z),i(z,i(y,z))))). 6 [hyper,4,1,2] P(i(i(i(x,i(y,z)),i(i(u,y),i(v,y))),i(w,i(i(u,y),i(v,y))))). 7 [hyper,5,1,5] P(i(i(x,y),i(y,i(x,y)))). 12 [hyper,7,1,2] P(i(i(i(x,i(y,x)),y),i(z,y))). 15 [hyper,6,1,12] P(i(x,i(i(y,z),i(z,z)))). 19 [hyper,6,1,2] P(i(i(i(x,i(i(y,z),i(u,z))),i(v,i(z,w))),i(v6,i(v,i(z,w))))). 20 [hyper,15,1,15] P(i(i(x,y),i(y,y))). 23 [hyper,20,1,12] P(i(i(x,y),i(x,y))). 24 [hyper,20,1,2] P(i(i(i(x,x),y),i(z,y))). 26 [hyper,23,1,2] P(i(i(i(x,y),x),i(z,x))). 27 [hyper,24,1,24] P(i(x,i(y,i(z,z)))). 28 [hyper,24,1,23] P(i(x,i(y,y))). 31 [hyper,24,1,4] P(i(x,i(y,i(z,y)))). 32 [hyper,28,1,28] P(i(x,x)). 38 [hyper,31,1,32] P(i(x,i(y,x))). 41 [hyper,38,1,27] P(i(x,i(y,i(z,i(u,u))))). 45 [hyper,38,1,2] P(i(x,i(i(i(y,z),u),i(i(u,y),i(v,y))))). 47 [hyper,38,1,2] P(i(i(i(x,i(y,z)),y),i(u,y))). 48 [hyper,26,1,2] P(i(i(i(x,y),i(y,z)),i(u,i(y,z)))). 53 [hyper,41,1,38] P(i(x,i(y,i(z,i(u,i(v,v)))))). 61 [hyper,19,1,2] P(i(x,i(i(i(i(y,z),i(u,z)),v),i(z,v)))). 80 [hyper,47,1,2] P(i(i(i(x,y),i(z,i(y,u))),i(v,i(z,i(y,u))))). 85 [hyper,53,1,38] P(i(x,i(y,i(z,i(u,i(v,i(w,w))))))). 92 [hyper,48,1,2] P(i(i(i(x,i(y,z)),i(u,y)),i(v,i(u,y)))). 122 [hyper,45,1,2] P(i(i(i(i(i(x,y),z),i(i(z,x),i(u,x))),v),i(w,v))). 130 [hyper,61,1,85] P(i(i(i(i(x,y),i(z,y)),u),i(y,u))). 138 [hyper,130,1,26] P(i(x,i(y,i(z,x)))). 139 [hyper,130,1,2] P(i(x,i(i(i(y,x),z),i(u,z)))). 166 [hyper,138,1,2] P(i(i(i(x,i(y,i(z,u))),z),i(v,z))). 338 [hyper,92,1,2] P(i(x,i(i(i(i(y,z),u),z),i(y,z)))). 353 [hyper,338,1,338] P(i(i(i(i(x,y),z),y),i(x,y))). 362 [hyper,353,1,2] P(i(i(i(x,y),i(i(x,y),z)),i(u,i(i(x,y),z)))). 970 [hyper,362,1,47] P(i(x,i(i(i(y,i(z,u)),z),z))). 973 [hyper,362,1,26] P(i(x,i(i(i(y,z),y),y))). 974 [hyper,362,1,24] P(i(x,i(i(i(y,y),z),z))). 991 [hyper,973,1,973] P(i(i(i(x,y),x),x)). 1004 [hyper,991,1,2] P(i(i(x,i(x,y)),i(z,i(x,y)))). 1005 [hyper,974,1,991] P(i(i(i(x,x),y),y)). 1016 [hyper,970,1,1005] P(i(i(i(x,i(y,z)),y),y)). 1027 [hyper,1016,1,2] P(i(i(x,i(y,i(x,z))),i(u,i(y,i(x,z))))). 1072 [hyper,1004,1,1004] P(i(x,i(i(y,i(y,z)),i(y,z)))). 1083 [hyper,1072,1,1072] P(i(i(x,i(x,y)),i(x,y))). 1104 [hyper,1083,1,166] P(i(i(i(x,i(y,i(z,u))),z),z)). 1114 [hyper,1083,1,92] P(i(i(i(x,i(y,z)),i(u,y)),i(u,y))). 1118 [hyper,1083,1,80] P(i(i(i(x,y),i(z,i(y,u))),i(z,i(y,u)))). 1124 [hyper,1083,1,48] P(i(i(i(x,y),i(y,z)),i(y,z))). 1155 [hyper,1104,1,2] P(i(i(x,i(y,i(z,i(x,u)))),i(v,i(y,i(z,i(x,u)))))). 1177 [hyper,1124,1,2] P(i(i(i(x,y),i(z,x)),i(u,i(z,x)))). 1374 [hyper,1177,1,1083] P(i(i(i(x,y),i(z,x)),i(z,x))). 1565 [hyper,1027,1,139] P(i(x,i(i(i(y,z),u),i(z,u)))). 1566 [hyper,1027,1,2] P(i(x,i(i(y,z),i(i(i(z,u),y),z)))). 1567 [hyper,1027,1,1083] P(i(i(x,i(y,i(x,z))),i(y,i(x,z)))). 1577 [hyper,1565,1,1565] P(i(i(i(x,y),z),i(y,z))). 1588 [hyper,1577,1,2] P(i(x,i(i(x,y),i(z,y)))). 1592 [hyper,1577,1,122] P(i(x,i(y,i(i(y,z),i(u,z))))). 1645 [hyper,1588,1,2] P(i(i(i(i(i(x,y),z),i(u,z)),x),i(v,x))). 1661 [hyper,1566,1,1592] P(i(i(x,y),i(i(i(y,z),x),y))). 1672 [hyper,1661,1,1588] P(i(i(i(i(i(x,y),i(z,y)),u),x),i(i(x,y),i(z,y)))). 1703 [hyper,1661,1,1004] P(i(i(i(i(x,i(y,z)),u),i(y,i(y,z))),i(x,i(y,z)))). 1741 [hyper,1661,1,138] P(i(i(i(i(x,i(y,z)),u),z),i(x,i(y,z)))). 1762 [hyper,1661,1,47] P(i(i(i(i(x,y),z),i(i(u,i(y,v)),y)),i(x,y))). 1765 [hyper,1661,1,26] P(i(i(i(i(x,y),z),i(i(y,u),y)),i(x,y))). 2492 [hyper,1645,1,1083] P(i(i(i(i(i(x,y),z),i(u,z)),x),x)). 4636 [hyper,1762,1,2492] P(i(i(i(i(i(x,i(i(y,z),u)),i(y,z)),v),z),i(y,z))). 7184 [hyper,1155,1,1083] P(i(i(x,i(y,i(z,i(x,u)))),i(y,i(z,i(x,u))))). 10842 [hyper,4636,1,1765] P(i(i(i(x,i(i(i(y,z),y),u)),i(i(y,z),y)),y)). 10924 [hyper,10842,1,1672] P(i(i(x,y),i(i(i(x,z),x),y))). 10927 [hyper,10924,1,1588] P(i(i(i(x,y),x),i(i(x,z),i(u,z)))). 10951 [hyper,10927,1,1741] P(i(x,i(y,i(i(x,z),i(u,z))))). 10953 [hyper,10927,1,1703] P(i(x,i(i(x,y),y))). 11237 [hyper,10953,1,10924] P(i(i(i(x,y),x),i(i(x,z),z))). 11252 [hyper,10953,1,1661] P(i(i(i(i(i(x,y),y),z),x),i(i(x,y),y))). 11310 [hyper,10951,1,1577] P(i(x,i(y,i(i(i(z,x),u),i(v,u))))). 11344 [hyper,11237,1,1741] P(i(x,i(y,i(i(x,z),z)))). 11355 [hyper,11237,1,2] P(i(i(i(i(x,y),y),i(x,z)),i(u,i(x,z)))). 11414 [hyper,11344,1,1577] P(i(x,i(y,i(i(i(z,x),u),u)))). 12034 [hyper,11355,1,1083] P(i(i(i(i(x,y),y),i(x,z)),i(x,z))). 12131 [hyper,12034,1,11414] P(i(x,i(i(i(y,i(i(x,z),z)),u),u))). 12134 [hyper,12034,1,11310] P(i(x,i(i(i(y,i(i(x,z),z)),u),i(v,u)))). 12136 [hyper,12034,1,10951] P(i(x,i(i(i(i(x,y),y),z),i(u,z)))). 12188 [hyper,12131,1,1374] P(i(i(i(x,i(i(i(y,z),u),u)),y),y)). 12191 [hyper,12131,1,1114] P(i(i(i(x,i(i(i(y,i(z,u)),v),v)),z),z)). 12238 [hyper,12136,1,1567] P(i(i(i(i(x,y),y),z),i(x,z))). 12442 [hyper,12188,1,11252] P(i(i(x,i(i(i(x,y),z),z)),i(i(i(x,y),z),z))). 13088 [hyper,12134,1,1118] P(i(i(i(x,i(i(i(y,z),u),u)),v),i(z,v))). 13109 [hyper,12191,1,1672] P(i(i(x,y),i(i(i(z,i(x,u)),y),y))). 13927 [hyper,13088,1,1672] P(i(i(i(x,y),z),i(i(i(u,x),z),z))). 14592 [hyper,12442,1,13109] P(i(i(i(i(x,y),i(x,z)),y),y)). 14632 [hyper,14592,1,13927] P(i(i(i(x,i(i(y,z),i(y,u))),z),z)). 14829 [hyper,14632,1,1672] P(i(i(x,i(y,z)),i(i(y,x),i(y,z)))). 15113 [hyper,14829,1,10951] P(i(i(x,y),i(x,i(i(y,z),i(u,z))))). 16490 [hyper,15113,1,12238] P(i(x,i(i(x,y),i(i(y,z),i(u,z))))). 17865 [hyper,16490,1,7184] P(i(i(x,y),i(i(y,z),i(x,z)))). 17866 [binary,17865,3] . ------------ end of proof ------------- -------------- statistics ------------- clauses input 3 clauses given 3096 clauses generated 8341570 demod & eval rewrites 0 clauses wt,lit,sk delete 2972221 tautologies deleted 0 clauses forward subsumed 5351487 (subsumed by sos) 83872 clauses kept 17862 new demodulators 0 empty clauses 1 clauses back demodulated 0 clauses back subsumed 386 sos size 14449 Kbytes malloced 10729 ----------- times (seconds) ----------- run time 7714.75 (run time 2 hr, 8 min, 34 sec) system time 1863.38 input time 0.01 clausify time 0.00 hyper_res time 2863.86 pre_process time 4227.72 demod time 0.00 weigh cl time 736.90 for_sub time 1461.46 renumber time 866.73 keep cl time 33.44 print_cl time 0.00 conflict time 4.74 post_process time 455.12 back demod time 0.00 back_sub time 450.01 lex_rpo time 0.00 The job finished Wed Jun 3 17:07:15 1992 \end{verbatim} } \subsection{Theorem 6: Many-valued Sentential Calculus, CD-57} {\small \begin{verbatim} ----- OTTER 2.2, July 1991 ----- The job began on altair.mcs.anl.gov, Wed Jun 3 13:16:52 1992 The command was "otter22". set(hyper_res). set(back_demod). set(dynamic_demod_all). clear(print_kept). assign(pick_given_ratio,5). assign(max_mem,20000). set(control_memory). list(usable). 1 [] -P(x) | -P(i(x,y)) | P(y). end_of_list. list(sos). 2 [] P(i(x,i(y,x))). 3 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 4 [] P(i(i(i(x,y),y),i(i(y,x),x))). 5 [] P(i(i(n(x),n(y)),i(y,x))). 6 [] -P(i(i(a,b),i(i(c,a),i(c,b)))). end_of_list. OTTER sets dynamic_demod, because back_demod is set. OTTER sets order_eq, because dynamic_demod is set. ----> UNIT CONFLICT at 17.68 sec ----> 4844 [binary,4843,6] . Level of proof is 4, length is 5. ---------------- PROOF ---------------- 1 [] -P(x) | -P(i(x,y)) | P(y). 2 [] P(i(x,i(y,x))). 3 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 4 [] P(i(i(i(x,y),y),i(i(y,x),x))). 6 [] -P(i(i(a,b),i(i(c,a),i(c,b)))). 14 [hyper,3,1,3] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 15 [hyper,3,1,2] P(i(i(i(x,y),z),i(y,z))). 24 [hyper,4,1,15] P(i(x,i(i(x,y),y))). 49 [hyper,24,1,3] P(i(i(i(i(x,y),y),z),i(x,z))). 4843 [hyper,49,1,14] P(i(i(x,y),i(i(z,x),i(z,y)))). 4844 [binary,4843,6] . ------------ end of proof ------------- -------------- statistics ------------- clauses input 6 clauses given 181 clauses generated 16687 demod & eval rewrites 0 tautologies deleted 0 clauses forward subsumed 11850 (subsumed by sos) 1683 clauses kept 4837 new demodulators 0 empty clauses 1 clauses back demodulated 0 clauses back subsumed 11 sos size 4650 Kbytes malloced 2171 ----------- times (seconds) ----------- run time 17.69 (run time 0 hr, 0 min, 17 sec) system time 4.34 input time 0.02 clausify time 0.00 hyper_res time 3.53 pre_process time 10.57 demod time 0.00 weigh cl time 0.00 for_sub time 2.80 renumber time 0.92 keep cl time 4.46 print_cl time 0.00 conflict time 1.17 post_process time 2.63 back demod time 0.00 back_sub time 2.57 lex_rpo time 0.00 The job finished Wed Jun 3 13:17:14 1992 \end{verbatim} } \subsection{Theorem 7: Many-valued Sentential Calculus, CD-60} {\small \begin{verbatim} ----- OTTER 2.2, July 1991 ----- The job began on altair.mcs.anl.gov, Wed Jun 3 13:31:24 1992 The command was "otter22". set(hyper_res). set(back_demod). set(dynamic_demod_all). clear(print_kept). assign(pick_given_ratio,5). assign(max_mem,20000). set(control_memory). list(usable). 1 [] -P(x) | -P(i(x,y)) | P(y). end_of_list. list(sos). 2 [] P(i(x,i(y,x))). 3 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 4 [] P(i(i(i(x,y),y),i(i(y,x),x))). 5 [] P(i(i(n(x),n(y)),i(y,x))). 6 [] -P(i(i(a,b),i(n(b),n(a)))). end_of_list. OTTER sets dynamic_demod, because back_demod is set. OTTER sets order_eq, because dynamic_demod is set. Resetting weight limit to 13. ----> UNIT CONFLICT at 2184.96 sec ----> 16257 [binary,16256,6] . Level of proof is 13, length is 24. ---------------- PROOF ---------------- 1 [] -P(x) | -P(i(x,y)) | P(y). 2 [] P(i(x,i(y,x))). 3 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 4 [] P(i(i(i(x,y),y),i(i(y,x),x))). 5 [] P(i(i(n(x),n(y)),i(y,x))). 6 [] -P(i(i(a,b),i(n(b),n(a)))). 7 [hyper,2,1,2] P(i(x,i(y,i(z,y)))). 13 [hyper,3,1,5] P(i(i(i(x,y),z),i(i(n(y),n(x)),z))). 14 [hyper,3,1,3] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 15 [hyper,3,1,2] P(i(i(i(x,y),z),i(y,z))). 18 [hyper,4,1,7] P(i(i(i(x,i(y,x)),z),z)). 21 [hyper,15,1,5] P(i(n(x),i(x,y))). 22 [hyper,15,1,4] P(i(x,i(i(x,y),y))). 27 [hyper,21,1,3] P(i(i(i(x,y),z),i(n(x),z))). 33 [hyper,22,1,5] P(i(i(i(i(n(x),n(y)),i(y,x)),z),z)). 37 [hyper,22,1,3] P(i(i(i(i(x,y),y),z),i(x,z))). 59 [hyper,18,1,15] P(i(x,x)). 63 [hyper,59,1,22] P(i(i(i(x,x),y),y)). 238 [hyper,13,1,63] P(i(i(n(x),n(i(y,y))),x)). 284 [hyper,238,1,27] P(i(n(n(x)),x)). 320 [hyper,284,1,5] P(i(x,n(n(x)))). 321 [hyper,284,1,3] P(i(i(x,y),i(n(n(x)),y))). 378 [hyper,320,1,22] P(i(i(i(x,n(n(x))),y),y)). 1651 [hyper,378,1,14] P(i(i(x,y),i(x,n(n(y))))). 1762 [hyper,33,1,14] P(i(i(x,i(n(y),n(z))),i(x,i(z,y)))). 2121 [hyper,37,1,14] P(i(i(x,i(y,z)),i(y,i(x,z)))). 3351 [hyper,1651,1,37] P(i(x,i(i(x,y),n(n(y))))). 5608 [hyper,3351,1,321] P(i(n(n(x)),i(i(x,y),n(n(y))))). 15901 [hyper,5608,1,2121] P(i(i(x,y),i(n(n(x)),n(n(y))))). 16256 [hyper,1762,1,15901] P(i(i(x,y),i(n(y),n(x)))). 16257 [binary,16256,6] . ------------ end of proof ------------- -------------- statistics ------------- clauses input 6 clauses given 2768 clauses generated 3214280 demod & eval rewrites 0 clauses wt,lit,sk delete 1712800 tautologies deleted 0 clauses forward subsumed 1485230 (subsumed by sos) 16917 clauses kept 16250 new demodulators 0 empty clauses 1 clauses back demodulated 0 clauses back subsumed 24 sos size 13466 Kbytes malloced 7216 ----------- times (seconds) ----------- run time 2185.01 (run time 0 hr, 36 min, 25 sec) system time 689.15 input time 0.00 clausify time 0.00 hyper_res time 845.48 pre_process time 1215.06 demod time 0.00 weigh cl time 271.12 for_sub time 272.29 renumber time 270.75 keep cl time 18.23 print_cl time 0.00 conflict time 3.61 post_process time 26.66 back demod time 0.00 back_sub time 25.92 lex_rpo time 0.00 The job finished Wed Jun 3 14:26:09 1992 \end{verbatim} } \section{Summary of Otter Outputs for the Equality Set} \subsection{Theorem EQ-1: The Commutator Theorem} {\small \begin{verbatim} ----- OTTER 2.2, July 1991 ----- The job began on altair.mcs.anl.gov, Fri Jun 5 14:33:33 1992 The command was "otter22". set(knuth_bendix). set(index_for_back_demod). set(process_input). assign(max_mem,16000). set(control_memory). set(lex_rpo). clear(print_kept). clear(print_new_demod). clear(print_back_demod). lex([a,b,e,f(x,x),g(x),h(x,x)]). lrpo_lr_status([f(x,x)]). list(usable). 0 [] (x = x). 0 [] (f(e,x) = x). 0 [] (f(g(x),x) = e). 0 [] (f(f(x,y),z) = f(x,f(y,z))). 0 [] (h(x,y) = f(x,f(y,f(g(x),g(y))))). end_of_list. list(sos). 0 [] (f(x,f(x,x)) = e). 0 [] (h(h(a,b),b) != e). end_of_list. OTTER sets dynamic_demod_all, because knuth_bendix is set. OTTER clears para_into_right, because knuth_bendix is set. OTTER sets back_demod, because knuth_bendix is set. OTTER sets para_from, because knuth_bendix is set. OTTER sets para_into, because knuth_bendix is set. OTTER clears para_from_right, because knuth_bendix is set. OTTER sets dynamic_demod, because back_demod is set. OTTER sets order_eq, because dynamic_demod is set. ------------> process usable: ** KEPT: 1 [] (x = x). ++++ cannot make into demodulator: 1 [] (x = x). ** KEPT: 2 [] (f(e,x) = x). ** KEPT: 4 [] (f(g(x),x) = e). ** KEPT: 6 [] (f(f(x,y),z) = f(x,f(y,z))). ** KEPT: 8 [] (h(x,y) = f(x,f(y,f(g(x),g(y))))). ------------> process sos: ** KEPT: 10 [] (f(x,f(x,x)) = e). ** KEPT: 12 [demod,9,9,7,7,7] (f(a,f(b,f(g(a),f(g(b),f(b,f(g(f(a,f(b,f(g(a), g(b))))),g(b))))))) != e). ------------> done processing input. ----> UNIT CONFLICT at 1.49 sec ----> 156 [binary,155,1] . Level of proof is 13, length is 19. ---------------- PROOF ---------------- 1 [] (x = x). 3,2 [] (f(e,x) = x). 5,4 [] (f(g(x),x) = e). 7,6 [] (f(f(x,y),z) = f(x,f(y,z))). 9,8 [] (h(x,y) = f(x,f(y,f(g(x),g(y))))). 11,10 [] (f(x,f(x,x)) = e). 12 [demod,9,9,7,7,7] (f(a,f(b,f(g(a),f(g(b),f(b,f(g(f(a,f(b,f(g(a),g(b))))),g(b))))))) != e). 13 [para_into,10,6,demod,7] (f(x,f(y,f(x,f(y,f(x,y))))) = e). 16,15 [para_from,10,6,demod,3,7] (f(y,f(y,f(y,x))) = x). 18,17 [para_into,15,10] (f(x,f(x,e)) = f(x,x)). 21 [para_into,15,4,demod,18] (f(g(x),g(x)) = x). 24,23 [para_into,15,10] (f(x,e) = x). 28,27 [para_from,21,6] (f(g(x),f(g(x),y)) = f(x,y)). 32,31 [para_into,27,21,demod,5] (f(x,g(x)) = e). 34,33 [para_into,27,15,demod,28] (f(g(x),y) = f(x,f(x,y))). 36,35 [para_into,27,10,demod,24,34,32,24] (g(x) = f(x,x)). 37 [back_demod,12,demod,36,36,36,36,7,36,7,7,7,7,7,36,7,7,7,7,7,7,7,7,7,7,7,11,24,7,16,7,16] (f(a,f(b,f(b,f(a,f(a,f(b,f(b,f(a,f(b,f(a,f(a,b))))))))))) != e). 43,42 [para_from,13,15,demod,24] (f(y,f(x,f(y,f(x,y)))) = f(x,x)). 45,44 [para_into,42,6,demod,7,7] (f(x,f(y,f(z,f(x,f(y,f(z,x)))))) = f(y,f(z,f(y,z)))). 48,47 [para_from,42,6,demod,7,7,7,7] (f(z,f(x,f(z,f(x,f(z,y))))) = f(x,f(x,y))). 56 [para_into,47,10,demod,24] (f(x,f(y,f(x,y))) = f(y,f(y,f(x,x)))). 62 [para_into,56,56,demod,7,7,16,11,24,7,7,7,7] (f(y,f(x,f(y,f(y,f(x,f(y,f(x,x))))))) = f(x,y)). 127 [para_from,62,47,demod,48] (f(x,f(y,f(y,x))) = f(y,f(x,f(x,y)))). 153,152 [para_from,127,56,demod,7,7,7,7,11,24,7,7] (f(x,f(y,f(y,f(x,f(y,f(x,f(x,y))))))) = f(y,f(y,f(x,f(y,y))))). 155 [back_demod,37,demod,153,45,43,11] (e != e). 156 [binary,155,1] . ------------ end of proof ------------- -------------- statistics ------------- clauses input 7 clauses given 19 clauses generated 542 demod & eval rewrites 1945 tautologies deleted 0 clauses forward subsumed 453 (subsumed by sos) 31 clauses kept 114 new demodulators 41 empty clauses 1 clauses back demodulated 18 clauses back subsumed 0 sos size 79 Kbytes malloced 255 ----------- times (seconds) ----------- run time 1.53 (run time 0 hr, 0 min, 1 sec) system time 0.28 input time 0.01 clausify time 0.00 process input 0.02 para_into time 0.10 para_from time 0.03 pre_process time 1.22 demod time 0.55 weigh cl time 0.00 for_sub time 0.06 renumber time 0.05 keep cl time 0.31 print_cl time 0.01 conflict time 0.03 post_process time 0.11 back demod time 0.04 back_sub time 0.07 lex_rpo time 0.13 The job finished Fri Jun 5 14:33:35 1992 \end{verbatim} } \subsection{Theorem EQ-2: Robbins Algebra, $(\exists c, c+c=c) \rightarrow$ Boolean} {\small \begin{verbatim} ----- OTTER 2.2, July 1991 ----- The job began on altair.mcs.anl.gov, Fri Jun 5 14:29:55 1992 The command was "otter22". set(knuth_bendix). set(index_for_back_demod). set(process_input). assign(max_mem,16000). set(control_memory). set(lex_rpo). clear(print_kept). clear(print_new_demod). clear(print_back_demod). lex([a,b,c,o(x,x),n(x)]). lrpo_lr_status([o(x,x)]). list(usable). 0 [] (x = x). 0 [] (o(x,y) = o(y,x)). 0 [] (o(o(x,y),z) = o(x,o(y,z))). 0 [] (n(o(n(o(x,y)),n(o(x,n(y))))) = x). end_of_list. list(sos). 0 [] (o(c,c) = c). 0 [] (o(n(o(a,n(b))),n(o(n(a),n(b)))) != b). end_of_list. OTTER sets dynamic_demod_all, because knuth_bendix is set. OTTER clears para_into_right, because knuth_bendix is set. OTTER sets back_demod, because knuth_bendix is set. OTTER sets para_from, because knuth_bendix is set. OTTER sets para_into, because knuth_bendix is set. OTTER clears para_from_right, because knuth_bendix is set. OTTER sets dynamic_demod, because back_demod is set. OTTER sets order_eq, because dynamic_demod is set. ------------> process usable: ** KEPT: 1 [] (x = x). ++++ cannot make into demodulator: 1 [] (x = x). ** KEPT: 2 [] (o(x,y) = o(y,x)). ++++ cannot make into demodulator: 2 [] (o(x,y) = o(y,x)). ** KEPT: 3 [] (o(o(x,y),z) = o(x,o(y,z))). ** KEPT: 5 [] (n(o(n(o(x,y)),n(o(x,n(y))))) = x). ------------> process sos: ** KEPT: 7 [] (o(c,c) = c). ** KEPT: 9 [] (o(n(o(a,n(b))),n(o(n(a),n(b)))) != b). ------------> done processing input. Resetting weight limit to 18. Resetting weight limit to 17. ----> UNIT CONFLICT at 98.19 sec ----> 7578 [binary,7577,1] . Level of proof is 31, length is 62. ---------------- PROOF ---------------- 1 [] (x = x). 2 [] (o(x,y) = o(y,x)). 4,3 [] (o(o(x,y),z) = o(x,o(y,z))). 5 [] (n(o(n(o(x,y)),n(o(x,n(y))))) = x). 8,7 [] (o(c,c) = c). 9 [] (o(n(o(a,n(b))),n(o(n(a),n(b)))) != b). 10 [para_from,7,5] (n(o(n(c),n(o(c,n(c))))) = c). 13,12 [para_from,7,3] (o(c,o(c,x)) = o(c,x)). 15,14 [para_into,12,2] (o(c,o(x,c)) = o(c,x)). 16 [para_from,12,5] (n(o(n(o(c,x)),n(o(c,n(o(c,x)))))) = c). 18 [para_into,14,3] (o(c,o(x,o(y,c))) = o(c,o(x,y))). 20 [para_from,14,5] (n(o(n(o(c,x)),n(o(c,n(o(x,c)))))) = c). 23,22 [para_from,14,3,demod,4,4] (o(c,o(x,o(c,y))) = o(c,o(x,y))). 26 [para_into,10,2] (n(o(n(o(c,n(c))),n(c))) = c). 28 [para_from,10,5] (n(o(n(o(n(c),o(c,n(c)))),c)) = n(c)). 42 [para_from,26,5] (n(o(n(o(n(o(c,n(c))),c)),c)) = n(o(c,n(c)))). 45,44 [para_from,26,5] (n(o(n(o(x,o(n(o(c,n(c))),n(c)))),n(o(x,c)))) = x). 56 [para_into,18,2,demod,4,23] (o(c,o(x,y)) = o(c,o(y,x))). 57 [para_into,18,2,demod,4,4,8] (o(x,o(y,c)) = o(c,o(x,y))). 64 [para_into,56,2,demod,4] (o(x,o(y,c)) = o(c,o(y,x))). 68 [para_from,56,2,demod,4] (o(c,o(x,y)) = o(y,o(x,c))). 70 [para_into,57,2] (o(x,o(c,y)) = o(c,o(x,y))). 71 [para_into,57,2,demod,4] (o(x,o(c,y)) = o(c,o(y,x))). 72 [para_from,57,5] (n(o(n(o(c,o(x,y))),n(o(x,n(o(y,c)))))) = x). 76 [para_from,57,2,demod,4] (o(c,o(x,y)) = o(y,o(c,x))). 82 [para_from,64,5] (n(o(n(o(c,o(x,y))),n(o(y,n(o(x,c)))))) = y). 86 [para_from,64,2,demod,4] (o(c,o(x,y)) = o(x,o(c,y))). 105 [para_into,76,68] (o(x,o(y,c)) = o(x,o(c,y))). 114 [para_into,86,76] (o(x,o(c,y)) = o(y,o(c,x))). 163 [para_into,9,2] (o(n(o(n(b),a)),n(o(n(a),n(b)))) != b). 166 [para_into,28,71] (n(o(n(o(c,o(n(c),n(c)))),c)) = n(c)). 168 [para_into,28,2] (n(o(c,n(o(n(c),o(c,n(c)))))) = n(c)). 180 [para_into,163,2] (o(n(o(n(b),a)),n(o(n(b),n(a)))) != b). 187 [para_from,166,5] (n(o(n(c),n(o(n(o(c,o(n(c),n(c)))),n(c))))) = n(o(c,o(n(c),n(c))))). 190,189 [para_from,168,5,demod,23] (n(o(n(o(c,o(n(c),n(c)))),n(c))) = c). 196,195 [back_demod,187,demod,190] (n(o(c,o(n(c),n(c)))) = n(o(n(c),c))). 201 [back_demod,166,demod,196] (n(o(n(o(n(c),c)),c)) = n(c)). 210,209 [para_into,201,2] (n(o(n(o(c,n(c))),c)) = n(c)). 212,211 [back_demod,42,demod,210] (n(o(n(c),c)) = n(o(c,n(c)))). 219 [back_demod,195,demod,212] (n(o(c,o(n(c),n(c)))) = n(o(c,n(c)))). 230 [para_into,219,68] (n(o(n(c),o(n(c),c))) = n(o(c,n(c)))). 240 [para_into,16,114,demod,8,13] (n(o(n(o(x,c)),n(o(c,n(o(c,x)))))) = c). 276 [para_into,20,2] (n(o(n(o(c,x)),n(o(n(o(x,c)),c)))) = c). 1150 [para_into,240,2] (n(o(n(o(x,c)),n(o(n(o(c,x)),c)))) = c). 2492 [para_into,72,105,demod,13,8] (n(o(n(o(c,x)),n(o(x,n(c))))) = x). 2517,2516 [para_into,72,276] (n(o(n(o(c,o(n(o(c,x)),n(o(x,c))))),c)) = n(o(c,x))). 2590 [para_into,2492,114,demod,8,4] (n(o(n(o(x,c)),n(o(c,o(x,n(c)))))) = o(c,x)). 2636 [para_into,2492,2] (n(o(n(o(c,x)),n(o(n(c),x)))) = x). 2642 [para_into,2492,2] (n(o(n(o(x,n(c))),n(o(c,x)))) = x). 2788 [para_into,2636,230,demod,15] (n(o(n(o(c,n(c))),n(o(c,n(c))))) = o(n(c),c)). 3454 [para_into,82,1150,demod,2517] (n(o(c,x)) = n(o(x,c))). 3508 [para_from,3454,5] (n(o(n(o(c,x)),n(o(n(x),c)))) = c). 3777 [para_into,3508,2] (n(o(n(o(n(x),c)),n(o(c,x)))) = c). 3912,3911 [para_into,3777,26,demod,8] (n(o(n(c),n(o(c,o(n(o(c,n(c))),n(c)))))) = c). 5861 [para_into,2590,209,demod,3912] (o(c,n(o(c,n(c)))) = c). 5928 [para_from,5861,70] (o(c,o(x,n(o(c,n(c))))) = o(x,c)). 5983,5982 [para_from,5928,2642,demod,4,45] (o(x,n(o(c,n(c)))) = x). 6005,6004 [back_demod,2788,demod,5983] (n(n(o(c,n(c)))) = o(n(c),c)). 6015,6014 [para_into,5982,2] (o(n(o(c,n(c))),x) = x). 6039,6038 [para_from,5982,5,demod,6005] (n(o(n(x),n(o(x,o(n(c),c))))) = x). 6040 [para_from,6014,5,demod,6015] (n(o(n(x),n(n(x)))) = n(o(c,n(c)))). 7006 [para_into,6040,6038,demod,6039] (n(o(x,n(x))) = n(o(c,n(c)))). 7023 [para_into,7006,2] (n(o(n(x),x)) = n(o(c,n(c)))). 7066 [para_from,7006,5,demod,6015] (n(n(o(x,n(n(x))))) = x). 7147,7146 [para_into,7066,2] (n(n(o(n(n(x)),x))) = x). 7416,7415 [para_from,7023,5,demod,5983,7147] (n(n(x)) = x). 7576,7575 [para_into,7415,5] (o(n(o(x,y)),n(o(x,n(y)))) = n(x)). 7577 [back_demod,180,demod,7576,7416] (b != b). 7578 [binary,7577,1] . ------------ end of proof ------------- -------------- statistics ------------- clauses input 6 clauses given 249 clauses generated 50001 demod & eval rewrites 122587 clauses wt,lit,sk delete 901 tautologies deleted 0 clauses forward subsumed 45667 (subsumed by sos) 10963 clauses kept 4548 new demodulators 3029 empty clauses 1 clauses back demodulated 1109 clauses back subsumed 3 sos size 3290 Kbytes malloced 5652 ----------- times (seconds) ----------- run time 98.31 (run time 0 hr, 1 min, 38 sec) system time 18.22 input time 0.01 clausify time 0.00 process input 0.03 para_into time 6.66 para_from time 4.05 pre_process time 63.38 demod time 24.30 weigh cl time 0.19 for_sub time 7.08 renumber time 3.83 keep cl time 8.73 print_cl time 0.00 conflict time 0.63 post_process time 22.50 back demod time 16.85 back_sub time 5.52 lex_rpo time 9.34 The job finished Fri Jun 5 14:31:54 1992 \end{verbatim} } \subsection{Theorem EQ-3: On Ternary Boolean Algebra} {\small \begin{verbatim} ----- OTTER 2.2, July 1991 ----- The job began on altair.mcs.anl.gov, Fri Jun 5 07:39:41 1992 The command was "otter22". set(knuth_bendix). set(index_for_back_demod). set(process_input). assign(max_mem,16000). set(control_memory). set(lex_rpo). clear(print_kept). clear(print_new_demod). clear(print_back_demod). lex([a,b,c,f(x,x,x),g(x)]). lrpo_lr_status([f(x,x,x)]). list(usable). 0 [] (x = x). end_of_list. list(sos). 0 [] (f(f(v,w,x),y,f(v,w,z)) = f(v,w,f(x,y,z))). 0 [] (f(y,x,x) = x). 0 [] (f(x,x,y) = x). 0 [] (f(g(y),y,x) = x). 0 [] (f(a,g(a),b) != b). end_of_list. OTTER sets dynamic_demod_all, because knuth_bendix is set. OTTER clears para_into_right, because knuth_bendix is set. OTTER sets back_demod, because knuth_bendix is set. OTTER sets para_from, because knuth_bendix is set. OTTER sets para_into, because knuth_bendix is set. OTTER clears para_from_right, because knuth_bendix is set. OTTER sets dynamic_demod, because back_demod is set. OTTER sets order_eq, because dynamic_demod is set. ------------> process usable: ** KEPT: 1 [] (x = x). ++++ cannot make into demodulator: 1 [] (x = x). ------------> process sos: ** KEPT: 2 [] (f(f(x,y,z),u,f(x,y,v)) = f(x,y,f(z,u,v))). ** KEPT: 4 [] (f(x,y,y) = y). ** KEPT: 6 [] (f(x,x,y) = x). ** KEPT: 8 [] (f(g(x),x,y) = y). ** KEPT: 10 [] (f(a,g(a),b) != b). ------------> done processing input. ----> UNIT CONFLICT at 16.78 sec ----> 1950 [binary,1948,10] . Level of proof is 11, length is 19. ---------------- PROOF ---------------- 3,2 [] (f(f(x,y,z),u,f(x,y,v)) = f(x,y,f(z,u,v))). 5,4 [] (f(x,y,y) = y). 7,6 [] (f(x,x,y) = x). 9,8 [] (f(g(x),x,y) = y). 10 [] (f(a,g(a),b) != b). 12,11 [para_into,2,6,demod,7,7] (f(x,y,x) = x). 16 [para_into,2,4] (f(f(x,y,z),u,y) = f(x,y,f(z,u,y))). 21,20 [para_into,2,6] (f(x,y,f(z,f(x,y,z),u)) = f(x,y,z)). 24 [para_from,11,2] (f(f(x,y,z),u,x) = f(x,y,f(z,u,x))). 50 [para_into,16,11] (f(x,z,f(x,y,z)) = f(x,y,z)). 53,52 [para_into,16,2] (f(f(x,y,f(z,u,v)),w,u) = f(f(x,y,z),u,f(f(x,y,v),w,u))). 82 [para_into,20,4] (f(x,y,f(x,y,z)) = f(x,y,z)). 90 [para_from,20,50,demod,21] (f(x,f(y,f(x,z,y),u),f(x,z,y)) = f(x,z,y)). 102 [para_from,82,2,demod,3] (f(x,y,f(z,u,f(x,y,v))) = f(x,y,f(z,u,v))). 351,350 [para_from,90,20,demod,5] (f(x,f(y,z,x),y) = f(y,z,x)). 386,385 [para_from,350,24] (f(f(x,y,z),u,z) = f(z,f(x,y,z),f(x,u,z))). 445 [para_into,102,20,demod,5] (f(x,f(y,z,x),f(y,z,u)) = f(y,z,x)). 506,505 [para_into,445,50] (f(x,f(y,z,x),f(y,u,z)) = f(y,z,x)). 524,523 [para_into,445,4] (f(x,f(y,z,x),z) = f(y,z,x)). 781 [para_from,505,350,demod,506] (f(f(x,y,z),f(x,z,u),u) = f(x,z,u)). 1301 [para_into,781,523,demod,53,12,524,524] (f(f(x,y,z),u,f(z,u,x)) = f(z,u,x)). 1734 [para_into,1301,523] (f(f(x,y,z),u,f(y,u,z)) = f(y,u,z)). 1855 [para_into,1734,8,demod,386,9] (f(z,f(x,g(y),z),f(x,y,z)) = z). 1948 [para_into,1855,6,demod,351] (f(y,g(y),x) = x). 1950 [binary,1948,10] . ------------ end of proof ------------- -------------- statistics ------------- clauses input 6 clauses given 47 clauses generated 3945 demod & eval rewrites 6838 tautologies deleted 0 clauses forward subsumed 3103 (subsumed by sos) 19 clauses kept 1030 new demodulators 919 empty clauses 1 clauses back demodulated 182 clauses back subsumed 3 sos size 798 Kbytes malloced 1564 ----------- times (seconds) ----------- run time 16.81 (run time 0 hr, 0 min, 16 sec) system time 1.85 input time 0.01 clausify time 0.00 process input 0.02 para_into time 0.50 para_from time 0.43 pre_process time 11.37 demod time 6.77 weigh cl time 0.00 for_sub time 0.92 renumber time 0.28 keep cl time 1.41 print_cl time 0.00 conflict time 0.17 post_process time 4.32 back demod time 3.01 back_sub time 1.30 lex_rpo time 0.40 The job finished Fri Jun 5 07:40:00 1992 \end{verbatim} } \subsection{Theorem EQ-4: Group Theory Single Axiom} {\small \begin{verbatim} ----- OTTER 2.2, July 1991 ----- The job began on altair.mcs.anl.gov, Fri Jun 5 07:36:59 1992 The command was "otter22". set(knuth_bendix). set(index_for_back_demod). set(process_input). assign(max_mem,16000). set(control_memory). set(lex_rpo). clear(print_kept). clear(print_new_demod). clear(print_back_demod). lex([a,b,c,f(x,x),i(x)]). lrpo_lr_status([f(x,x)]). list(usable). 0 [] (x = x). end_of_list. list(sos). 0 [] (f(x,i(f(f(i(f(i(y),f(i(x),w))),z),i(f(y,z))))) = w). 0 [] (f(a,f(b,c)) != f(f(a,b),c)). end_of_list. OTTER sets dynamic_demod_all, because knuth_bendix is set. OTTER clears para_into_right, because knuth_bendix is set. OTTER sets back_demod, because knuth_bendix is set. OTTER sets para_from, because knuth_bendix is set. OTTER sets para_into, because knuth_bendix is set. OTTER clears para_from_right, because knuth_bendix is set. OTTER sets dynamic_demod, because back_demod is set. OTTER sets order_eq, because dynamic_demod is set. ------------> process usable: ** KEPT: 1 [] (x = x). ++++ cannot make into demodulator: 1 [] (x = x). ------------> process sos: ** KEPT: 2 [] (f(x,i(f(f(i(f(i(y),f(i(x),z))),u),i(f(y,u))))) = z). ** KEPT: 4 [] (f(f(a,b),c) != f(a,f(b,c))). ------------> done processing input. ----> UNIT CONFLICT at 44.12 sec ----> 4092 [binary,4090,4] . Level of proof is 50, length is 92. ---------------- PROOF ---------------- 3,2 [] (f(x,i(f(f(i(f(i(y),f(i(x),z))),u),i(f(y,u))))) = z). 4 [] (f(f(a,b),c) != f(a,f(b,c))). 5 [para_into,2,2] (f(x,i(f(f(i(f(i(y),z)),u),i(f(y,u))))) = i(f(f(i(f(i(v), f(i(i(x)),z))),w),i(f(v,w))))). 12 [para_into,5,5] (f(x,i(f(i(f(f(i(f(i(y),f(i(i(i(f(i(z),u)))),v))),w), i(f(y,w)))),i(f(z,i(f(f(i(f(i(v6),v)),v7),i(f(v6,v7))))))))) = i(f(f(i(f(i(v8),f(i(i(x)),u))),v9),i(f(v8,v9))))). 19,18 [para_into,5,2] (i(f(f(i(f(i(y),f(i(i(z)),f(i(z),x)))),u),i(f(y,u)))) = x). 29 [para_into,18,18,demod,19] (i(f(f(i(f(i(x),f(i(y),f(y,w)))),v6),i(f(x,v6)))) = w). 48 [para_into,29,5] (i(f(i(f(f(i(f(i(x),f(i(i(i(f(i(y),f(i(z),f(z,u)))))),v))), w),i(f(x,w)))),i(f(y,i(f(f(i(f(i(v6),v)),v7),i(f(v6,v7)))))))) = u). 50 [para_into,29,2] (i(f(x,i(f(y,i(f(f(i(f(i(z),f(i(i(f(i(y),f(i(u),f(u,v))))), x))),w),i(f(z,w)))))))) = v). 60 [para_from,29,5] (i(f(f(i(f(i(z),f(i(i(x)),f(i(u),f(u,y))))),v),i(f(z,v)))) = f(x,y)). 81 [para_into,60,5] (i(f(i(f(f(i(f(i(x),f(i(i(i(f(i(y),f(i(i(z)),f(i(u), f(u,v))))))),w))),v6),i(f(x,v6)))),i(f(y,i(f(f(i(f(i(v7),w)), v8),i(f(v7,v8)))))))) = f(z,v)). 98,97 [para_from,60,5] (i(f(f(i(f(i(u),f(i(i(x)),f(i(i(y)),f(i(v),f(v,z)))))), w),i(f(u,w)))) = f(x,f(y,z))). 99 [para_from,60,2] (f(i(x),f(x,y)) = f(i(z),f(z,y))). 114 [para_into,99,99] (f(i(i(x)),f(i(y),f(y,z))) = f(i(u),f(u,f(x,z)))). 116,115 [para_into,99,5,demod,3] (f(i(v),f(v,i(f(f(i(f(i(w),z)),v6),i(f(w,v6)))))) = z). 125 [para_from,99,29] (i(f(f(i(f(i(x),f(x,f(y,z)))),u),i(f(i(y),u)))) = z). 136 [para_from,99,2] (f(x,i(f(f(i(f(i(y),f(y,z))),u),i(f(i(x),u))))) = z). 146 [para_from,114,60,demod,98] (f(y,f(i(z),f(z,v))) = f(y,f(i(v6),f(v6,v)))). 158 [para_into,146,99] (f(x,f(i(i(y)),f(i(z),f(z,u)))) = f(x,f(i(v),f(v,f(y,u))))). 160 [para_from,146,99] (f(i(x),f(x,f(i(y),f(y,z)))) = f(i(u),f(u,f(i(v),f(v,z))))). 210 [para_into,115,99] (f(i(x),f(x,i(f(f(i(f(i(y),f(y,z))),u),i(f(v,u)))))) = f(v,z)). 221,220 [para_into,115,99] (f(i(x),f(x,i(f(f(i(y),f(y,z)),i(f(u,f(f(i(u),v),z))))))) = v). 224 [para_into,115,2] (f(i(x),f(x,i(f(y,i(f(z,i(f(f(i(f(i(u),f(i(i(f(i(z),v))), y))),w),i(f(u,w)))))))))) = v). 300,299 [para_into,125,99] (i(f(f(i(f(i(x),f(x,f(y,z)))),f(y,u)),i(f(i(v),f(v,u))))) = z). 355 [para_into,136,99] (f(x,i(f(f(i(y),f(y,z)),i(f(i(x),f(f(i(u),f(u,v)),z)))))) = v). 1301 [para_into,355,220,demod,221] (f(f(i(x),f(x,y)),i(f(v6,i(v6)))) = y). 1410 [para_from,1301,210] (f(i(f(i(x),f(x,y))),y) = f(i(f(i(z),f(z,u))),u)). 1434 [para_from,1301,220] (f(i(x),f(x,i(f(f(i(f(i(y),f(y,z))),z),i(f(u, f(f(i(u),v),i(f(w,i(w)))))))))) = v). 1436 [para_from,1301,114] (f(i(i(x)),f(i(f(i(y),f(y,z))),z)) = f(i(u),f(u,f(x,i(f(v,i(v))))))). 1484 [para_from,1410,355] (f(f(i(x),f(x,f(f(i(y),f(y,z)),u))),i(f(f(i(v), f(v,u)),i(f(i(f(i(w),f(w,v6))),v6))))) = z). 1489,1488 [para_from,1410,220,demod,221] (f(i(i(v)),f(i(f(i(w),f(w,v6))),v6)) = v). 1493,1492 [para_from,1410,210] (f(i(x),f(x,i(f(f(i(f(i(y),f(y,z))),z),i(f(u,v)))))) = f(u,v)). 1541 [back_demod,1436,demod,1489] (f(i(u),f(u,f(x,i(f(v,i(v)))))) = x). 1545,1544 [back_demod,1434,demod,1493] (f(u,f(f(i(u),v),i(f(w,i(w))))) = v). 1591 [para_from,1541,1301] (f(x,i(f(y,i(y)))) = f(x,i(f(z,i(z))))). 1675 [para_into,1544,5] (f(x,f(i(f(f(i(f(i(y),f(i(i(i(x))),z))),u),i(f(y,u)))), i(f(v,i(v))))) = i(f(f(i(f(i(w),z)),v6),i(f(w,v6))))). 1802 [para_from,1488,210] (f(i(x),f(x,i(f(f(i(f(i(y),f(y,z))),f(i(f(i(u), f(u,v))),v)),i(w))))) = f(i(i(w)),z)). 1857 [para_from,1591,1488] (f(i(i(x)),f(i(f(i(y),f(y,i(f(z,i(z)))))),i(f(u,i(u))))) = x). 1884 [para_from,1591,115,demod,116] (i(f(z,i(z))) = i(f(v,i(v)))). 1948 [para_from,1884,1488,demod,1489] (f(x,i(x)) = f(u,i(u))). 1969 [para_from,1884,99] (f(i(f(x,i(x))),f(f(y,i(y)),z)) = f(i(u),f(u,z))). 2010 [para_from,1948,1544] (f(x,f(y,i(y))) = i(i(x))). 2107 [para_into,2010,99] (f(i(x),f(x,i(y))) = i(i(i(y)))). 2116 [para_from,2010,299] (i(f(i(i(i(f(i(x),f(x,f(y,z)))))),i(f(i(u),f(u,i(y)))))) = z). 2131 [para_from,2010,210] (f(i(x),f(x,i(f(i(i(i(f(i(y),f(y,z))))),i(f(u,f(v,i(v)))))))) = f(u,z)). 2368 [para_into,2107,299,demod,300] (f(i(x),f(x,y)) = i(i(y))). 2373 [para_into,2368,1884] (f(i(f(x,i(x))),f(f(y,i(y)),z)) = i(i(z))). 2381,2380 [para_into,2368,2368] (i(i(f(x,y))) = f(i(i(x)),i(i(y)))). 2401 [para_into,2368,158,demod,2381,2381,2381] (f(i(x),f(x,f(i(y),f(y,f(z,u))))) = f(i(i(i(i(z)))),f(i(i(i(v))),f(i(i(v)),i(i(u)))))). 2438 [back_demod,2131,demod,2381,2381] (f(i(x),f(x,i(f(i(f(i(i(i(y))),f(i(i(y)), i(i(z))))),i(f(u,f(v,i(v)))))))) = f(u,z)). 2446 [back_demod,2116,demod,2381,2381,2381] (i(f(i(f(i(i(i(x))),f(i(i(x)),f(i(i(y)), i(i(z)))))),i(f(i(u),f(u,i(y)))))) = z). 2587 [back_demod,224,demod,2381] (f(i(x),f(x,i(f(y,i(f(z,i(f(f(i(f(i(u),f(f(i(i(i(z))), i(i(v))),y))),w),i(f(u,w)))))))))) = v). 2598 [back_demod,81,demod,2381,2381,2381,2381] (i(f(i(f(f(i(f(i(x),f(i(f(i(i(i(y))), f(i(i(i(i(z)))),f(i(i(i(u))),f(i(i(u)),i(i(v))))))),w))),v6),i(f(x,v6)))), i(f(y,i(f(f(i(f(i(v7),w)),v8),i(f(v7,v8)))))))) = f(z,v)). 2604 [back_demod,50,demod,2381,2381,2381] (i(f(x,i(f(y,i(f(f(i(f(i(z),f(f(i(i(i(y))), f(i(i(i(u))),f(i(i(u)),i(i(v))))),x))),w),i(f(z,w)))))))) = v). 2606 [back_demod,48,demod,2381,2381,2381] (i(f(i(f(f(i(f(i(x),f(i(f(i(i(i(y))), f(i(i(i(z))),f(i(i(z)),i(i(u)))))),v))),w),i(f(x,w)))),i(f(y, i(f(f(i(f(i(v6),v)),v7),i(f(v6,v7)))))))) = u). 2617 [back_demod,12,demod,2381] (f(x,i(f(i(f(f(i(f(i(y),f(i(f(i(i(i(z))),i(i(u)))), v))),w),i(f(y,w)))),i(f(z,i(f(f(i(f(i(v6),v)),v7),i(f(v6,v7))))))))) = i(f(f(i(f(i(v8),f(i(i(x)),u))),v9),i(f(v8,v9))))). 2621 [para_from,2368,1488] (i(i(x)) = f(i(y),f(y,x))). 2633 [para_from,2368,210] (f(i(x),f(x,i(f(i(i(y)),i(f(z,f(f(i(u),f(u,v)),y))))))) = f(z,v)). 2647 [para_from,2368,1301] (f(i(i(x)),i(f(y,i(y)))) = x). 2706 [para_from,2368,160] (f(i(x),f(x,f(i(i(y)),i(i(z))))) = f(i(u),f(u,f(i(v),f(v,f(y,z)))))). 2709 [para_from,2368,29] (i(f(f(i(f(i(x),i(i(y)))),z),i(f(x,z)))) = y). 2802,2801 [para_from,2621,1488] (f(i(f(i(x),f(x,y))),f(i(f(i(z),f(z,u))),u)) = i(y)). 2866,2865 [back_demod,1802,demod,2802] (f(i(x),f(x,i(f(i(z),i(w))))) = f(i(i(w)),z)). 2873 [back_demod,2633,demod,2866,2381,2381,2381,2381] (f(f(i(i(z)),f(f(i(i(i(u))), f(i(i(u)),i(i(v)))),i(i(y)))),i(y)) = f(z,v)). 2879 [back_demod,2438,demod,2866,2381,2381] (f(f(i(i(u)),f(i(i(v)),i(i(i(v))))), f(i(i(i(y))),f(i(i(y)),i(i(z))))) = f(u,z)). 2884,2883 [para_into,2647,2621] (f(i(f(i(x),f(x,y))),i(f(z,i(z)))) = i(y)). 2921,2920 [back_demod,1857,demod,2884,2381] (f(i(i(x)),f(i(i(z)),i(i(i(z))))) = x). 2929,2928 [back_demod,2879,demod,2921] (f(x,f(i(i(i(z))),f(i(i(z)),i(i(u))))) = f(x,u)). 2938,2937 [back_demod,2606,demod,2929] (i(f(i(f(f(i(f(i(x),f(i(f(i(i(i(y))),u)),v))),w), i(f(x,w)))),i(f(y,i(f(f(i(f(i(v6),v)),v7),i(f(v6,v7)))))))) = u). 2940,2939 [back_demod,2604,demod,2929] (i(f(x,i(f(y,i(f(f(i(f(i(z),f(f(i(i(i(y))), v),x))),w),i(f(z,w)))))))) = v). 2944,2943 [back_demod,2598,demod,2929,2938] (f(i(i(i(i(z)))),v) = f(z,v)). 2978,2977 [back_demod,2401,demod,2929,2944] (f(i(x),f(x,f(i(y),f(y,f(z,u))))) = f(z,u)). 2985,2984 [back_demod,2617,demod,2938] (i(f(f(i(f(i(v8),f(i(i(x)),u))),v9),i(f(v8,v9)))) = f(x,i(i(u)))). 2987,2986 [back_demod,2587,demod,2940] (f(i(x),f(x,i(i(v)))) = v). 3017,3016 [back_demod,2706,demod,2978] (f(i(x),f(x,f(i(i(y)),i(i(z))))) = f(y,z)). 3114,3113 [back_demod,1675,demod,2985,1545] (i(f(f(i(f(i(w),z)),v6),i(f(w,v6)))) = i(i(z))). 3204 [back_demod,2873,demod,2987] (f(f(i(i(x)),f(z,i(i(u)))),i(u)) = f(x,z)). 3266 [back_demod,2446,demod,3017] (i(f(i(f(y,z)),i(f(i(u),f(u,i(y)))))) = z). 3344,3343 [back_demod,2709,demod,3114] (i(i(i(i(y)))) = y). 3706,3705 [para_into,3343,2621] (i(f(i(x),f(x,i(y)))) = y). 3711 [back_demod,3266,demod,3706] (i(f(i(f(x,y)),x)) = y). 3752 [para_from,3343,1591] (f(x,i(f(i(i(i(y))),y))) = f(x,i(f(z,i(z))))). 3759 [para_into,3711,1544] (i(f(i(x),y)) = f(f(i(y),x),i(f(z,i(z))))). 3773,3772 [para_into,3711,2010,demod,2381,2381,2381,2381,3344,3344,3344] (f(f(x,i(x)),y) = y). 3814 [back_demod,2373,demod,3773] (f(i(f(x,i(x))),z) = i(i(z))). 3825 [back_demod,1969,demod,3773] (f(i(f(x,i(x))),z) = f(i(u),f(u,z))). 3896,3895 [para_into,3772,1884,demod,3773] (f(i(f(y,i(y))),z) = z). 3900,3899 [para_into,3772,1544,demod,3896] (f(x,i(f(z,i(z)))) = x). 3914,3913 [back_demod,3825,demod,3896] (f(i(z),f(z,y)) = y). 3920,3919 [back_demod,3814,demod,3896] (i(i(y)) = y). 3935,3934 [back_demod,3759,demod,3900] (i(f(i(x),y)) = f(i(y),x)). 3937,3936 [back_demod,3752,demod,3920,3935,3900] (f(x,f(i(y),y)) = x). 4029 [back_demod,3204,demod,3920,3920] (f(f(x,f(y,z)),i(z)) = f(x,y)). 4042 [back_demod,1484,demod,3914,3914,3914,3914,3935,3937] (f(f(z,u),i(u)) = z). 4090 [para_into,4029,4042,demod,3920] (f(f(x,y),z) = f(x,f(y,z))). 4092 [binary,4090,4] . ------------ end of proof ------------- -------------- statistics ------------- clauses input 3 clauses given 57 clauses generated 3417 demod & eval rewrites 9814 tautologies deleted 0 clauses forward subsumed 3327 (subsumed by sos) 503 clauses kept 2507 new demodulators 1584 empty clauses 1 clauses back demodulated 2414 clauses back subsumed 61 sos size 15 Kbytes malloced 4470 ----------- times (seconds) ----------- run time 89.93 (run time 0 hr, 1 min, 29 sec) system time 3.46 input time 0.01 clausify time 0.00 process input 0.01 para_into time 0.69 para_from time 0.83 pre_process time 71.63 demod time 7.86 weigh cl time 0.00 for_sub time 1.73 renumber time 0.84 keep cl time 9.14 print_cl time 0.00 conflict time 0.32 post_process time 16.45 back demod time 14.77 back_sub time 1.43 lex_rpo time 2.54 The job finished Fri Jun 5 07:38:34 1992 \end{verbatim} } \subsection{Theorem EQ-5: On Wajsberg Algebra} {\small \begin{verbatim} ----- OTTER 2.2, July 1991 ----- The job began on altair.mcs.anl.gov, Thu Jun 4 17:31:43 1992 The command was "otter22". set(knuth_bendix). set(index_for_back_demod). set(process_input). assign(max_mem,16000). set(control_memory). set(lex_rpo). clear(print_kept). clear(print_new_demod). clear(print_back_demod). lex([a,b,T,i(x,x),n(x)]). lrpo_lr_status([i(x,x)]). list(usable). 0 [] (x = x). end_of_list. list(sos). 0 [] (i(T,x) = x). 0 [] (i(i(x,y),i(i(y,z),i(x,z))) = T). 0 [] (i(i(x,y),y) = i(i(y,x),x)). 0 [] (i(i(n(x),n(y)),i(y,x)) = T). 0 [] (i(i(i(a,b),i(b,a)),i(b,a)) != T). end_of_list. OTTER sets dynamic_demod_all, because knuth_bendix is set. OTTER clears para_into_right, because knuth_bendix is set. OTTER sets back_demod, because knuth_bendix is set. OTTER sets para_from, because knuth_bendix is set. OTTER sets para_into, because knuth_bendix is set. OTTER clears para_from_right, because knuth_bendix is set. OTTER sets dynamic_demod, because back_demod is set. OTTER sets order_eq, because dynamic_demod is set. ------------> process usable: ** KEPT: 1 [] (x = x). ++++ cannot make into demodulator: 1 [] (x = x). ------------> process sos: ** KEPT: 2 [] (i(T,x) = x). ** KEPT: 4 [] (i(i(x,y),i(i(y,z),i(x,z))) = T). ** KEPT: 6 [] (i(i(x,y),y) = i(i(y,x),x)). ++++ cannot make into demodulator: 6 [] (i(i(x,y),y) = i(i(y,x),x)). ** KEPT: 7 [] (i(i(n(x),n(y)),i(y,x)) = T). ** KEPT: 9 [] (i(i(i(a,b),i(b,a)),i(b,a)) != T). ------------> done processing input. Resetting weight limit to 15. ----> UNIT CONFLICT at 2248.86 sec ----> 11462 [binary,11460,11350] . Level of proof is 37, length is 85. ---------------- PROOF ---------------- 3,2 [] (i(T,x) = x). 4 [] (i(i(x,y),i(i(y,z),i(x,z))) = T). 6 [] (i(i(x,y),y) = i(i(y,x),x)). 7 [] (i(i(n(x),n(y)),i(y,x)) = T). 9 [] (i(i(i(a,b),i(b,a)),i(b,a)) != T). 10 [para_into,6,6] (i(i(i(x,y),y),x) = i(i(x,i(y,x)),i(y,x))). 12 [para_into,6,2] (i(i(x,T),T) = i(x,x)). 21 [para_into,7,2] (i(i(n(x),n(T)),x) = T). 23 [para_from,7,6,demod,3] (i(i(i(x,y),i(n(y),n(x))),i(n(y),n(x))) = i(x,y)). 25 [para_into,21,6] (i(i(n(T),n(n(T))),n(n(T))) = T). 31 [para_from,21,6,demod,3] (i(i(x,i(n(x),n(T))),i(n(x),n(T))) = x). 35 [para_from,25,6,demod,3] (i(i(n(n(T)),i(n(T),n(n(T)))),i(n(T),n(n(T)))) = n(n(T))). 49 [para_into,4,2,demod,3] (i(x,i(i(x,y),y)) = T). 63 [para_into,4,2] (i(i(x,T),i(y,i(x,y))) = T). 92,91 [para_into,49,2,demod,3] (i(x,x) = T). 98,97 [para_into,49,12,demod,92] (i(x,T) = T). 102,101 [back_demod,63,demod,98,3] (i(y,i(x,y)) = T). 103 [back_demod,35,demod,102,3] (i(n(T),n(n(T))) = n(n(T))). 106,105 [back_demod,10,demod,102,3] (i(i(i(x,y),y),x) = i(y,x)). 111 [para_from,101,4,demod,3] (i(i(x,y),i(x,i(z,y))) = T). 113 [para_from,101,6,demod,3] (i(i(i(x,y),y),y) = i(x,y)). 115 [para_from,101,4,demod,3] (i(i(i(x,y),z),i(y,z)) = T). 151 [para_into,111,49,demod,3] (i(x,i(y,i(i(x,z),z))) = T). 194,193 [para_into,115,21,demod,3] (i(n(T),x) = T). 195 [para_into,115,7,demod,3] (i(n(x),i(x,y)) = T). 210,209 [back_demod,103,demod,194] (n(n(T)) = T). 219 [para_from,193,4,demod,3] (i(i(x,n(T)),i(x,y)) = T). 222,221 [para_from,193,6,demod,3] (i(i(x,n(T)),n(T)) = x). 229 [para_from,195,4,demod,3] (i(i(x,n(y)),i(x,i(y,z))) = T). 234,233 [para_from,195,6,demod,3] (i(i(i(x,y),n(x)),n(x)) = i(x,y)). 237 [para_from,221,7,demod,210,3] (i(n(i(x,n(T))),x) = T). 248,247 [para_from,237,7,demod,3] (i(x,i(n(x),n(T))) = T). 258,257 [back_demod,31,demod,248,3] (i(n(x),n(T)) = x). 259 [para_from,257,221] (i(x,n(T)) = n(x)). 264 [para_from,257,115] (i(i(i(x,n(y)),n(T)),y) = T). 272 [para_from,257,4,demod,194,3] (i(x,i(n(x),y)) = T). 275,274 [para_into,259,257] (n(n(x)) = x). 276 [para_into,259,221] (n(i(x,n(T))) = x). 278 [para_from,259,113,demod,222] (n(x) = i(x,n(T))). 288,287 [para_from,274,7] (i(i(n(x),y),i(n(y),x)) = T). 289 [para_from,274,7] (i(i(x,n(y)),i(y,n(x))) = T). 291 [para_from,278,7] (i(i(n(x),i(y,n(T))),i(y,x)) = T). 322,321 [para_from,219,6,demod,3] (i(i(i(x,y),i(x,n(T))),i(x,n(T))) = i(x,y)). 377 [para_into,151,6] (i(x,i(i(i(i(x,y),y),z),z)) = T). 417 [para_into,264,259] (i(n(i(x,n(y))),y) = T). 429 [para_into,417,274] (i(n(i(x,y)),n(y)) = T). 441 [para_into,429,6] (i(n(i(i(x,y),y)),n(x)) = T). 474,473 [para_into,287,274] (i(i(x,y),i(n(y),n(x))) = T). 479 [para_into,287,272,demod,275,3] (i(n(i(x,y)),x) = T). 491 [back_demod,23,demod,474,3] (i(n(y),n(x)) = i(x,y)). 496 [para_from,287,6,demod,3,288,3] (i(n(x),y) = i(n(y),x)). 500,499 [para_into,479,278] (i(i(i(x,y),n(T)),x) = T). 509 [para_into,491,278] (i(i(x,n(T)),n(y)) = i(y,x)). 511 [para_into,491,274] (i(x,n(y)) = i(y,n(x))). 513 [para_into,491,276] (i(n(x),y) = i(i(y,n(T)),x)). 520 [para_from,491,4] (i(i(n(x),y),i(i(y,n(z)),i(z,x))) = T). 530 [para_from,491,113,demod,234] (i(x,y) = i(n(y),n(x))). 533 [para_from,491,49] (i(n(x),i(i(y,x),n(y))) = T). 536,535 [para_from,491,6] (i(i(n(x),n(y)),n(y)) = i(i(x,y),n(x))). 540 [para_into,496,276] (i(x,y) = i(n(y),i(x,n(T)))). 565 [para_from,496,6] (i(i(n(x),y),x) = i(i(x,n(y)),n(y))). 569 [para_into,511,276] (i(x,y) = i(i(y,n(T)),n(x))). 598 [para_from,511,6] (i(i(x,n(y)),n(x)) = i(i(n(x),y),y)). 624,623 [para_into,530,105] (i(n(y),n(i(i(y,x),x))) = i(x,y)). 627 [para_into,530,6] (i(n(x),n(i(y,x))) = i(i(x,y),y)). 647 [para_from,530,4] (i(i(x,y),i(i(n(z),n(y)),i(x,z))) = T). 723 [para_into,289,278] (i(i(x,i(y,n(T))),i(y,n(x))) = T). 726,725 [para_into,289,530] (i(n(i(x,n(y))),n(i(y,n(x)))) = T). 771 [para_from,441,6,demod,3,624] (i(i(y,x),n(i(i(x,y),y))) = n(x)). 808 [para_into,509,276] (i(i(x,n(T)),y) = i(i(y,n(T)),x)). 1005 [para_from,533,4,demod,3] (i(i(i(i(x,y),n(x)),z),i(n(y),z)) = T). 1464,1463 [para_into,229,569,demod,258] (i(i(x,n(y)),i(y,i(x,z))) = T). 1470,1469 [para_into,229,513,demod,258] (i(i(x,y),i(n(y),i(x,z))) = T). 2855 [para_into,9,530] (i(i(i(n(b),n(a)),i(b,a)),i(b,a)) != T). 7827,7826 [para_from,725,627,demod,275,726,3] (n(i(y,n(x))) = i(i(x,n(y)),n(T))). 8405,8404 [para_into,771,723,demod,1464,3,3,7827] (n(i(y,i(x,n(T)))) = i(i(y,n(x)),n(T))). 8431,8430 [para_into,771,291,demod,1470,3,8405,3] (n(i(x,y)) = i(i(n(y),n(x)),n(T))). 10857 [para_from,565,113,demod,106] (i(i(n(y),x),x) = i(i(n(x),y),x)). 10860 [para_from,10857,233,demod,8431,275,8431,275,322] (i(i(n(x),y),x) = i(i(n(y),x),x)). 10862 [para_into,10860,274,demod,536] (i(i(x,y),n(x)) = i(i(y,x),n(y))). 10887 [para_into,10862,496,demod,275] (i(i(n(x),y),y) = i(i(x,n(y)),n(x))). 10936 [para_from,10887,598,demod,275,8431,275,275,8431,275,275,500,3] (i(i(i(x,y),n(x)),i(i(y,x),n(T))) = y). 11090 [para_into,520,540,demod,258] (i(i(n(x),y),i(i(x,n(z)),i(z,y))) = T). 11114 [para_into,1005,647,demod,275,3] (i(n(x),i(i(n(y),z),i(i(z,x),y))) = T). 11184 [para_into,11090,808,demod,8431,275,3,258,258] (i(i(x,y),i(i(z,x),i(z,y))) = T). 11202 [para_from,11184,377,demod,3] (i(x,i(i(y,i(x,z)),i(y,z))) = T). 11213,11212 [para_into,11202,11202,demod,3] (i(i(x,i(y,z)),i(y,i(x,z))) = T). 11285 [para_from,11212,6,demod,3,11213,3] (i(x,i(y,z)) = i(y,i(x,z))). 11350 [para_from,11285,2855] (i(b,i(i(i(n(b),n(a)),i(b,a)),a)) != T). 11460 [para_into,11114,10936,demod,275,8431,275,8431,3,222] (i(x,i(i(i(n(x),n(y)),i(x,y)),y)) = T). 11462 [binary,11460,11350] . ------------ end of proof ------------- -------------- statistics ------------- clauses input 6 clauses given 768 clauses generated 1012625 demod & eval rewrites 2793093 clauses wt,lit,sk delete 249150 tautologies deleted 0 clauses forward subsumed 761142 (subsumed by sos) 1097 clauses kept 5897 new demodulators 5564 empty clauses 1 clauses back demodulated 3558 clauses back subsumed 18 sos size 1655 Kbytes malloced 6801 ----------- times (seconds) ----------- run time 2249.42 (run time 0 hr, 37 min, 29 sec) system time 344.04 input time 0.01 clausify time 0.00 process input 0.01 para_into time 122.66 para_from time 115.25 pre_process time 1927.16 demod time 1567.96 weigh cl time 37.51 for_sub time 56.03 renumber time 69.31 keep cl time 9.72 print_cl time 0.00 conflict time 1.43 post_process time 65.32 back demod time 53.96 back_sub time 10.91 lex_rpo time 76.22 The job finished Thu Jun 4 18:15:07 1992 \end{verbatim} } \section{Conclusion} Years of experimentation with theorem-proving systems\cite{mow,aura,itp,otter2-guide,otter22} has caused us to accumulate a wide variety of variations and parameters to control our basic theorem-proving algorithm. The typical user need know about only a few of them. This contest forced us to consider how we would set them if there were to be a parameterless version of OTTER. Most of the above settings just represent common sense. The value of {\tt max\_mem} did have to be carefully chosen so that we could get proofs of all of these theorems with the same value. \nocite{mow,cd-cade,itp,aura} \bibliographystyle{plain} % \bibliography{/home/mccune/papers/bib/master} \begin{thebibliography}{1} \bibitem{roo-exp} E.~Lusk and W.~McCune. \newblock Experiments with {{\sc Roo}}, a parallel automated deduction system. \newblock In B.~{Fronh\"ofer} and G.~Wrightson, editors, {\em Parallelization in Inference Systems, Lecture Notes in Artificial Intelligence, Vol. 590}, pages 139--162, New York, 1992. Springer-Verlag. \bibitem{roo-tm} E.~Lusk, W.~McCune, and J.~Slaney. \newblock {\sc Roo}---a parallel theorem prover. \newblock Tech. Memo MCS-TM-149, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, 1991. \bibitem{itp} E.~Lusk and R.~Overbeek. \newblock The automated reasoning system {ITP}. \newblock Tech. Report ANL-84/27, Argonne National Laboratory, Argonne, IL, April 1984. \bibitem{mow} J.~McCharen, R.~Overbeek, and L.~Wos. \newblock Problems and experiments for and with automated theorem-proving programs. \newblock {\em IEEE Transactions on Computers}, C-25(8):773--782, August 1976. \bibitem{otter2-guide} W.~McCune. \newblock {\sc Otter} 2.0 {U}sers {G}uide. \newblock Tech. Report ANL-90/9, Argonne National Laboratory, Argonne, IL, March 1990. \bibitem{otter22} W.~McCune. \newblock What's {N}ew in {{\sc Otter}} 2.2. \newblock Tech. Memo ANL/MCS-TM-153, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, July 1991. \bibitem{presence-absence} W.~McCune and L.~Wos. \newblock The absence and the presence of fixed point combinators. \newblock {\em Theoretical Computer Science}, 87:221--228, 1991. \bibitem{cd-cade} W.~McCune and L.~Wos. \newblock Experiments in automated deduction with condensed detachment. \newblock Preprint MCS-P237-0491, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, 1991. \newblock To appear in proc. CADE-11, Springer-Verlag LNAI. \bibitem{aura} B.~Smith. \newblock Reference manual for the environmental theorem prover: An incarnation of {AURA}. \newblock Tech. Report ANL-88-2, Argonne National Laboratory, Argonne, IL, March 1988. \end{thebibliography} \end{document}