WATCH: 0.00 CPU 0.01 WC ALERT: Will not run MODE-THM152-MS98-3 due to minimal CPU limit 4 ALERT: Will not run MODE-MODULAR-EQUIV-THM due to minimal CPU limit 4 ALERT: Will not run MODE-DISTRIB-THM-MS98 due to minimal CPU limit 4 ALERT: Will not run MODE-PENTAGON-THM2B due to minimal CPU limit 4 ALERT: Will not run MODE-CD-LATTICE-THM due to minimal CPU limit 4 ALERT: Will not run IND-SV-MODE3 due to minimal CPU limit 5 ALERT: Will not run COIND-SV-MODE-180 due to minimal CPU limit 5 ALERT: Will not run MODE-THM15B-V2 due to minimal CPU limit 5 ALERT: Will not run MODE-THM15A-1 due to minimal CPU limit 5 ALERT: Will not run SV-MODE-NOD1 due to minimal CPU limit 5 ALERT: Will not run MODE-THM119-MS98 due to minimal CPU limit 5 ALERT: Will not run MODE-THM409-1-MS90-3 due to minimal CPU limit 5 ALERT: Will not run MODE-THM574 due to minimal CPU limit 5 ALERT: Will not run MODE-THM112-B due to minimal CPU limit 5 ALERT: Will not run MODE-THM300-MSV due to minimal CPU limit 5 ALERT: Will not run MODE-X5204-MS98 due to minimal CPU limit 5 ALERT: Will not run MS98-THM568-MODE due to minimal CPU limit 5 ALERT: Will not run MODE-X2129-C due to minimal CPU limit 5 ALERT: Will not run MODE-PA-THM2-MS98 due to minimal CPU limit 5 ALERT: Will not run MODE-THM126-CORR due to minimal CPU limit 5 ALERT: Will not run MODE-THM145-B-1 due to minimal CPU limit 6 ALERT: Will not run MODE-EQUIV123-MS98 due to minimal CPU limit 6 CPU used so far: 0.15 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 2 4 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode CT29-MODE 2>&1 WATCH: 2.93 CPU 3.02 WC CPU used so far: 4.21 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 2 4 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MODE-THM631-2 2>&1 WATCH: 5.87 CPU 6.03 WC CPU used so far: 8.27 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 4 8 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MODE-X5202 2>&1 CPU used so far: 8.37 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 4 8 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MS03-TF-MODE 2>&1 WATCH: 8.79 CPU 9.04 WC WATCH: 11.80 CPU 12.05 WC CPU used so far: 14.48 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 4 8 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode PR00-MAX-MODE 2>&1 --- TPS did not prove conj using mode PR00-MAX-MODE. --- CPU used so far: 14.58 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 2 4 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode EASY-SV-MODE 2>&1 WATCH: 14.78 CPU 15.06 WC --- TPS did not prove conj using mode EASY-SV-MODE. --- CPU used so far: 15.27 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 5 10 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode M15B-TEMP6 2>&1 --- TPS did not prove conj using mode M15B-TEMP6. --- CPU used so far: 15.96 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 2 4 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MODE-X5310-A 2>&1 WATCH: 17.84 CPU 18.07 WC CPU used so far: 18.03 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 4 8 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MODE-MS04-2-EQ-PRIMSUB 2>&1 WATCH: 20.74 CPU 21.08 WC WATCH: 23.76 CPU 24.09 WC CPU used so far: 24.13 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 4 8 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode QUIET-SV-MS03-MODE 2>&1 WATCH: 26.69 CPU 27.10 WC WATCH: 29.71 CPU 30.11 WC CPU used so far: 30.22 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 4 8 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MODE-THM112A-PR00 2>&1 --- TPS did not prove conj using mode MODE-THM112A-PR00. --- CPU used so far: 30.35 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 5 10 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MODE-THM303-DTPS 2>&1 WATCH: 32.66 CPU 33.12 WC WATCH: 35.67 CPU 36.13 WC CPU used so far: 36.46 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 5 10 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MODE-X5309A-INTERACTIVE 2>&1 WATCH: 38.64 CPU 39.13 WC WATCH: 41.66 CPU 42.15 WC CPU used so far: 42.61 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 4 8 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MODE-THM131-MSV-A 2>&1 CPU used so far: 42.68 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 4 8 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MODE-THM584-PR00 2>&1 --- TPS did not prove conj using mode MODE-THM584-PR00. --- CPU used so far: 42.82 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 2 4 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MODE-CLOSED-THM1 2>&1 WATCH: 44.65 CPU 45.16 WC CPU used so far: 46.89 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 4 8 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode IND-SV-MODE 2>&1 WATCH: 47.59 CPU 48.17 WC WATCH: 50.62 CPU 51.19 WC CPU used so far: 51.03 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 2 4 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MODE-THM120I-1 2>&1 --- TPS did not prove conj using mode MODE-THM120I-1. --- CPU used so far: 51.13 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 2 4 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MS04-EQ-TESTMODE 2>&1 CPU used so far: 53.22 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 2 4 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MODE-THM270-MS98 2>&1 --- TPS did not prove conj using mode MODE-THM270-MS98. --- CPU used so far: 53.42 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 4 8 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MODE-THM302-DTPS 2>&1 CPU used so far: 53.52 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 4 8 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MODE-THM407-A 2>&1 WATCH: 53.52 CPU 54.20 WC WATCH: 56.57 CPU 57.22 WC CPU used so far: 57.71 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 4 8 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MODE-T145-MS98-7 2>&1 WATCH: 59.54 CPU 60.23 WC --- TPS did not prove conj using mode MODE-T145-MS98-7. --- CPU used so far: 61.61 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 5 10 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MODE-THM300A-4 2>&1 WATCH: 62.56 CPU 63.25 WC WATCH: 65.59 CPU 66.27 WC CPU used so far: 67.75 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 5 10 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode EASY-MS03-7-MODE 2>&1 WATCH: 68.52 CPU 69.28 WC WATCH: 71.54 CPU 72.30 WC CPU used so far: 73.88 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 2 4 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MODE-MODULAR-THM-MS98 2>&1 --- TPS did not prove conj using mode MODE-MODULAR-THM-MS98. --- CPU used so far: 73.98 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 2 4 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode THM135-MODE 2>&1 CPU used so far: 74.08 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 2 4 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MODE-THM122-PR97 2>&1 WATCH: 74.52 CPU 75.31 WC WATCH: 77.55 CPU 78.33 WC CPU used so far: 78.15 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 4 8 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MODE-THM577 2>&1 --- TPS did not prove conj using mode MODE-THM577. --- CPU used so far: 78.49 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 2 4 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode X5309-MS04-MODE-1 2>&1 WATCH: 80.48 CPU 81.35 WC CPU used so far: 82.54 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 4 8 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MODE-THM350 2>&1 WATCH: 83.43 CPU 84.36 WC WATCH: 86.43 CPU 87.37 WC CPU used so far: 86.65 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 5 10 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MODE-THM204 2>&1 CPU used so far: 86.72 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 5 10 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MODE-STRANGE-HO-EXAMPLE 2>&1 WATCH: 89.36 CPU 90.39 WC WATCH: 92.37 CPU 93.40 WC CPU used so far: 92.83 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 5 10 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MODE-THM532-2 2>&1 --- TPS did not prove conj using mode MODE-THM532-2. --- CPU used so far: 94.27 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 2 4 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MODE-THM40 2>&1 WATCH: 95.33 CPU 96.41 WC WATCH: 98.29 CPU 99.43 WC CPU used so far: 98.32 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 5 10 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MODE-THM531E 2>&1 WATCH: 101.27 CPU 102.44 WC WATCH: 104.30 CPU 105.45 WC CPU used so far: 104.45 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 2 4 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MODE-X5500 2>&1 --- TPS did not prove conj using mode MODE-X5500. --- CPU used so far: 104.53 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 4 8 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MODE-X5310-MS98 2>&1 --- TPS did not prove conj using mode MODE-X5310-MS98. --- CPU used so far: 105.96 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 4 8 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MODE-6102-MS98 2>&1 --- TPS did not prove conj using mode MODE-6102-MS98. --- CPU used so far: 106.05 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 2 4 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MODE-THM145-A-1 2>&1 WATCH: 106.08 CPU 108.46 WC WATCH: 108.30 CPU 111.48 WC CPU used so far: 108.69 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 2 4 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MODE-MS04-THM616-PREN-SUGG 2>&1 CPU used so far: 110.75 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 2 4 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MODE-S-JOINFN-MONOTONE 2>&1 WATCH: 110.76 CPU 114.49 WC --- TPS did not prove conj using mode MODE-S-JOINFN-MONOTONE. --- CPU used so far: 110.87 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 2 4 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode THM100-QUICK-MATING 2>&1 WATCH: 112.36 CPU 117.51 WC CPU used so far: 114.94 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 2 4 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MODE-THM89-MSV 2>&1 CPU used so far: 115.08 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 2 4 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MODE-X5211-REAL 2>&1 WATCH: 115.30 CPU 120.52 WC WATCH: 118.32 CPU 123.53 WC CPU used so far: 119.14 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 2 4 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MODE-THM522-MS98 2>&1 --- TPS did not prove conj using mode MODE-THM522-MS98. --- CPU used so far: 119.3 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 2 4 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode SV-TOPOL-MODE-PFTAC 2>&1 --- TPS did not prove conj using mode SV-TOPOL-MODE-PFTAC. --- CPU used so far: 120.02 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 2 4 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MS03-X5309-TEMP-MODE 2>&1 WATCH: 121.33 CPU 126.54 WC CPU used so far: 124.09 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 2 4 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MODE-THM173 2>&1 WATCH: 124.29 CPU 129.57 WC CPU used so far: 126.17 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 5 10 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MODE-GRP-COMM2-MS98 2>&1 --- TPS did not prove conj using mode MODE-GRP-COMM2-MS98. --- CPU used so far: 126.33 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 5 10 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode GAZING-MODE2 2>&1 WATCH: 127.24 CPU 132.58 WC WATCH: 130.29 CPU 135.59 WC CPU used so far: 132.52 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 5 10 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MODE-THM15B-PR97-A 2>&1 --- TPS did not prove conj using mode MODE-THM15B-PR97-A. --- CPU used so far: 133.21 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 5 10 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MODE-THM136-MS98 2>&1 --- TPS did not prove conj using mode MODE-THM136-MS98. --- CPU used so far: 133.29 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 5 10 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MS98-HO-MODE 2>&1 WATCH: 133.30 CPU 138.60 WC --- TPS did not prove conj using mode MS98-HO-MODE. --- CPU used so far: 133.43 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 5 10 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MS98-THM563-MODE 2>&1 --- TPS did not prove conj using mode MS98-THM563-MODE. --- CPU used so far: 135.2 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 5 10 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MODE-THM126-MS98 2>&1 --- TPS did not prove conj using mode MODE-THM126-MS98. --- CPU used so far: 136.19 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 4 8 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MODE-X5306A 2>&1 CPU used so far: 136.31 ----------------------------------------------------------------------------- RUNNING: /CW/home-0/sutcliff/SystemExecution/TreeLimitedRun -q2 -p2 163 326 0 /CW/external/nobackup/CASC/cmucl/bin/lisp -core /CW/home-0/sutcliff/Systems/TPS---3.110228S1a/Source/tps3 -prob /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps -mode MODE-THM252C 2>&1 WATCH: 136.35 CPU 141.61 WC % SZS status GaveUp for /tmp/TPS-GOOD1_28039_cl5-010/TEQ167.tps WATCH: 136.43 CPU 141.67 WC FINAL WATCH: 136.43 CPU 141.67 WC