Job 2039

CakeML:7c856c8d5772c495ba037ebfbc63c2bdd01c4d32
  Fix build-sequence, move fp related tools to separate folder [Nov 11 11:09:10]
#911 (libm_gen)
Merging into:3d27e77937edd037e810801a4e7849352300104f
  Add [schematic] to a definition (suggested by @mn200) [Nov 07 20:36:24]
HOL:126d898e2a2195a717f5757375b93570965286f1
  Cleanup and tweak release notes for next version in a few places [Nov 03 06:41:06]
Machine:oven3

Nov 11 11:09:40 Claimed job
Nov 11 11:09:42 Reusing HOL
Nov 11 11:10:37 Starting developers
Nov 11 11:10:46 Finished developers                                               8s 115MB
Nov 11 11:10:46 Starting developers/bin
Nov 11 11:10:59 Finished developers/bin                                          12s   1GB
Nov 11 11:10:59 Starting compiler/proofs
Nov 11 14:35:28 Finished compiler/proofs                                    3h24m28s  17GB
Nov 11 14:35:28 Starting compiler/bootstrap/translation
Nov 12 00:52:44 Finished compiler/bootstrap/translation                    10h17m15s  38GB
Nov 12 00:52:45 Starting semantics/ffi
Nov 12 00:52:52 Finished semantics/ffi                                            7s 231MB
Nov 12 00:52:52 Starting semantics
Nov 12 00:52:55 Finished semantics                                                2s  33MB
Nov 12 00:52:55 Starting semantics/proofs
Nov 12 00:54:08 Finished semantics/proofs                                      1m12s 956MB
Nov 12 00:54:08 Starting semantics/alt_semantics
Nov 12 00:55:05 Finished semantics/alt_semantics                                 56s 537MB
Nov 12 00:55:05 Starting semantics/alt_semantics/proofs
Nov 12 01:21:16 Finished semantics/alt_semantics/proofs                       26m10s   1GB
Nov 12 01:21:16 Starting basis/pure
Nov 12 01:21:19 Finished basis/pure                                               2s  31MB
Nov 12 01:21:19 Starting translator
Nov 12 01:25:03 Finished translator                                            3m43s   1GB
Nov 12 01:25:03 Starting compiler/parsing
Nov 12 01:25:05 Finished compiler/parsing                                         2s  17MB
Nov 12 01:25:06 Starting characteristic
Nov 12 01:25:09 Finished characteristic                                           3s  23MB
Nov 12 01:25:09 Starting translator/monadic
Nov 12 01:25:13 Finished translator/monadic                                       2s  35MB
Nov 12 01:25:13 Starting basis
Nov 12 01:32:45 Finished basis                                                 7m32s   3GB
Nov 12 01:32:45 Starting compiler/inference
Nov 12 01:32:48 Finished compiler/inference                                       2s  29MB
Nov 12 01:32:49 Starting compiler/backend/reg_alloc
Nov 12 01:32:51 Finished compiler/backend/reg_alloc                               2s  27MB
Nov 12 01:32:51 Starting compiler/backend/gc
Nov 12 01:32:56 Finished compiler/backend/gc                                      3s  24MB
Nov 12 01:32:56 Starting compiler/backend
Nov 12 01:33:21 Finished compiler/backend                                        24s 609MB
Nov 12 01:33:21 Starting compiler/encoders/asm
Nov 12 01:33:24 Finished compiler/encoders/asm                                    2s  31MB
Nov 12 01:33:24 Starting compiler/encoders/x64
Nov 12 01:33:27 Finished compiler/encoders/x64                                    2s  34MB
Nov 12 01:33:28 Starting compiler/encoders/arm7
Nov 12 01:33:31 Finished compiler/encoders/arm7                                   2s  36MB
Nov 12 01:33:31 Starting compiler/encoders/arm8
Nov 12 01:33:34 Finished compiler/encoders/arm8                                   2s  29MB
Nov 12 01:33:34 Starting compiler/encoders/arm8_asl
Nov 12 01:40:45 Finished compiler/encoders/arm8_asl                            7m10s   1GB
Nov 12 01:40:45 Starting compiler/encoders/mips
Nov 12 01:40:48 Finished compiler/encoders/mips                                   2s  26MB
Nov 12 01:40:48 Starting compiler/encoders/riscv
Nov 12 01:40:51 Finished compiler/encoders/riscv                                  2s  27MB
Nov 12 01:40:51 Starting compiler/encoders/ag32
Nov 12 01:40:54 Finished compiler/encoders/ag32                                   2s  28MB
Nov 12 01:40:54 Starting compiler/backend/x64
Nov 12 01:40:58 Finished compiler/backend/x64                                     3s  34MB
Nov 12 01:40:59 Starting compiler/backend/arm7
Nov 12 01:41:02 Finished compiler/backend/arm7                                    3s  30MB
Nov 12 01:41:02 Starting compiler/backend/arm8
Nov 12 01:41:06 Finished compiler/backend/arm8                                    3s  32MB
Nov 12 01:41:06 Starting compiler/backend/mips
Nov 12 01:41:10 Finished compiler/backend/mips                                    3s  30MB
Nov 12 01:41:10 Starting compiler/backend/riscv
Nov 12 01:41:13 Finished compiler/backend/riscv                                   2s  30MB
Nov 12 01:41:14 Starting compiler/backend/ag32
Nov 12 01:44:10 Finished compiler/backend/ag32                                 2m56s   1GB
Nov 12 01:44:11 Starting compiler/parsing/proofs
Nov 12 01:44:13 Finished compiler/parsing/proofs                                  2s  31MB
Nov 12 01:44:14 Starting compiler/inference/proofs
Nov 12 01:44:17 Finished compiler/inference/proofs                                2s  32MB
Nov 12 01:44:17 Starting compiler/backend/semantics
Nov 12 01:46:43 Finished compiler/backend/semantics                            2m25s   1GB
Nov 12 01:46:43 Starting compiler/backend/reg_alloc/proofs
Nov 12 01:46:46 Finished compiler/backend/reg_alloc/proofs                        3s  33MB
Nov 12 01:46:47 Starting compiler/backend/proofs
Nov 12 01:48:36 Finished compiler/backend/proofs                               1m48s   2GB
Nov 12 01:48:36 Starting compiler/backend/serialiser
Nov 12 01:48:41 Finished compiler/backend/serialiser                              4s  44MB
Nov 12 01:48:41 Starting compiler/encoders/x64/proofs
Nov 12 02:11:08 Finished compiler/encoders/x64/proofs                         22m25s   4GB
Nov 12 02:11:08 Starting compiler/encoders/arm7/proofs
Nov 12 02:41:42 Finished compiler/encoders/arm7/proofs                        30m33s   5GB
Nov 12 02:41:42 Starting compiler/encoders/arm8/proofs
Nov 12 02:57:27 Finished compiler/encoders/arm8/proofs                        15m44s   1GB
Nov 12 02:57:28 Starting compiler/encoders/arm8_asl/proofs
Nov 12 03:35:09 Finished compiler/encoders/arm8_asl/proofs                    37m40s   1GB
Nov 12 03:35:09 Starting compiler/encoders/mips/proofs
Nov 12 03:58:49 Finished compiler/encoders/mips/proofs                        23m39s   3GB
Nov 12 03:58:49 Starting compiler/encoders/riscv/proofs
Nov 12 04:19:22 Finished compiler/encoders/riscv/proofs                       20m32s   1GB
Nov 12 04:19:22 Starting compiler/encoders/ag32/proofs
Nov 12 04:25:18 Finished compiler/encoders/ag32/proofs                         5m55s 892MB
Nov 12 04:25:19 Starting compiler/backend/x64/proofs
Nov 12 04:26:13 Finished compiler/backend/x64/proofs                             53s   1GB
Nov 12 04:26:13 Starting compiler/backend/arm7/proofs
Nov 12 04:27:13 Finished compiler/backend/arm7/proofs                            59s   1GB
Nov 12 04:27:13 Starting compiler/backend/arm8/proofs
Nov 12 04:28:09 Finished compiler/backend/arm8/proofs                            56s   1GB
Nov 12 04:28:10 Starting compiler/backend/arm8_asl
Nov 12 04:29:07 Finished compiler/backend/arm8_asl                               57s   1GB
Nov 12 04:29:08 Starting compiler/backend/mips/proofs
Nov 12 04:30:05 Finished compiler/backend/mips/proofs                            57s   1GB
Nov 12 04:30:05 Starting compiler/backend/riscv/proofs
Nov 12 04:30:59 Finished compiler/backend/riscv/proofs                           54s   1GB
Nov 12 04:31:00 Starting compiler/backend/ag32/proofs
Nov 12 05:01:53 Finished compiler/backend/ag32/proofs                         30m52s   2GB
Nov 12 05:01:53 Starting candle/set-theory
Nov 12 05:03:00 Finished candle/set-theory                                     1m06s   1GB
Nov 12 05:03:01 Starting candle/syntax-lib
Nov 12 05:03:03 Finished candle/syntax-lib                                        2s  34MB
Nov 12 05:03:03 Starting candle/standard/syntax
Nov 12 05:03:24 Finished candle/standard/syntax                                  20s 519MB
Nov 12 05:03:25 Starting candle/standard/semantics
Nov 12 05:07:18 Finished candle/standard/semantics                             3m52s   1GB
Nov 12 05:07:18 Starting candle/standard/monadic
Nov 12 05:07:21 Finished candle/standard/monadic                                  3s  27MB
Nov 12 05:07:22 Starting candle/standard/ml_kernel
Nov 12 05:10:34 Finished candle/standard/ml_kernel                             3m12s   2GB
Nov 12 05:10:35 Starting candle/overloading/syntax
Nov 12 05:17:30 Finished candle/overloading/syntax                             6m55s   1GB
Nov 12 05:17:31 Starting candle/overloading/semantics
Nov 12 05:44:48 Finished candle/overloading/semantics                         27m17s   2GB
Nov 12 05:44:49 Starting candle/overloading/monadic
Nov 12 05:50:25 Finished candle/overloading/monadic                            5m36s   1GB
Nov 12 05:50:26 Starting candle/overloading/ml_kernel
Nov 12 06:06:04 Finished candle/overloading/ml_kernel                         15m38s   2GB
Nov 12 06:06:04 Starting candle/overloading/ml_checker
Nov 12 06:12:22 Finished candle/overloading/ml_checker                         6m17s   4GB
Nov 12 06:12:23 Starting candle/prover
Nov 12 06:34:11 Finished candle/prover                                        21m47s   2GB
Nov 12 06:34:11 Starting pancake
Nov 12 06:40:39 Finished pancake                                               6m28s   3GB
Nov 12 06:40:40 Starting pancake/ffi
Nov 12 06:40:40 Finished pancake/ffi                                              0s  14MB
Nov 12 06:40:41 Starting pancake/semantics
Nov 12 06:45:46 Finished pancake/semantics                                     5m05s   1GB
Nov 12 06:45:47 Starting pancake/proofs
Nov 12 06:52:06 Finished pancake/proofs                                        6m18s   1GB
Nov 12 06:52:06 Starting characteristic/examples
Nov 12 06:55:12 Finished characteristic/examples                               3m06s   3GB
Nov 12 06:55:13 Starting tutorial/solutions
Nov 12 07:30:41 Finished tutorial/solutions                                   35m27s  14GB
Nov 12 07:30:41 Starting translator/monadic/examples
Nov 14 10:06:25 Resuming translator/monadic/examples
Nov 14 10:06:28 Finished translator/monadic/examples                              2s  24MB
Nov 14 10:06:29 Starting examples
Nov 14 10:25:20 Finished examples                                             18m50s   4GB
Nov 14 10:25:20 Starting examples/compilation/x64
Nov 14 15:03:15 Finished examples/compilation/x64                           4h37m53s  21GB
Nov 14 15:03:15 Starting examples/compilation/x64/proofs
Nov 14 15:07:41 Finished examples/compilation/x64/proofs                       4m25s   3GB
Nov 14 15:07:41 Starting examples/compilation/ag32
Nov 14 16:23:00 Finished examples/compilation/ag32                          1h15m17s   9GB
Nov 14 16:23:00 Starting examples/compilation/ag32/proofs
Nov 14 16:24:44 Finished examples/compilation/ag32/proofs                      1m44s   3GB
Nov 14 16:24:45 Starting examples/compilation/to_word
Nov 14 16:31:39 Finished examples/compilation/to_word                          6m53s   3GB
Nov 14 16:31:39 Starting examples/lpr_checker
Nov 14 16:33:40 Finished examples/lpr_checker                                  2m00s 942MB
Nov 14 16:33:40 Starting examples/lpr_checker/array
Nov 14 17:53:15 Finished examples/lpr_checker/array                         1h19m34s   5GB
Nov 14 17:53:15 Starting examples/lpr_checker/array/compilation
Nov 14 19:14:49 Finished examples/lpr_checker/array/compilation             1h21m33s  32GB
Nov 14 19:14:49 Starting examples/lpr_checker/array/compilation/proofs
Nov 14 19:18:08 Finished examples/lpr_checker/array/compilation/proofs         3m18s   6GB
Nov 14 19:18:08 Starting examples/opentheory
Nov 14 19:40:49 Finished examples/opentheory                                  22m40s   5GB
Nov 14 19:40:49 Starting examples/opentheory
Nov 14 19:40:53 Finished examples/opentheory                                      3s  33MB
Nov 14 19:40:53 Starting examples/opentheory/compilation
Nov 14 21:04:43 Finished examples/opentheory/compilation                    1h23m49s  28GB
Nov 14 21:04:43 Starting examples/opentheory/compilation/proofs
Nov 14 21:06:43 Finished examples/opentheory/compilation/proofs                1m58s   3GB
Nov 14 21:06:43 Starting examples/opentheory/compilation/ag32
Nov 14 22:32:46 Finished examples/opentheory/compilation/ag32               1h26m02s  55GB
Nov 14 22:32:46 Starting examples/opentheory/compilation/ag32/proofs
Nov 14 22:37:11 Finished examples/opentheory/compilation/ag32/proofs           4m24s   6GB
Nov 14 22:37:11 Starting examples/sat_encodings
Nov 14 22:40:58 Finished examples/sat_encodings                                3m46s 788MB
Nov 14 22:40:59 Starting examples/sat_encodings/case_studies
Nov 14 22:44:28 Finished examples/sat_encodings/case_studies                   3m28s   1GB
Nov 14 22:44:28 Starting examples/sat_encodings/translation
Nov 14 22:56:22 Finished examples/sat_encodings/translation                   11m54s   5GB
Nov 14 22:56:23 Starting examples/sat_encodings/translation/compilation
Nov 15 00:22:50 Finished examples/sat_encodings/translation/compilation     1h26m27s  22GB
Nov 15 00:22:51 Starting examples/deflate
Nov 15 00:24:36 Finished examples/deflate                                      1m45s 819MB
Nov 15 00:24:37 Starting examples/deflate/translation
Nov 15 00:27:34 Finished examples/deflate/translation                          2m57s   3GB
Nov 15 00:27:34 Starting examples/deflate/translation/compilation
Nov 15 01:08:54 Finished examples/deflate/translation/compilation             41m19s  19GB
Nov 15 01:08:54 Starting translator/okasaki-examples
Nov 15 01:18:58 Finished translator/okasaki-examples                          10m03s   1GB
Nov 15 01:18:58 Starting translator/other-examples
Nov 15 01:20:29 Finished translator/other-examples                             1m30s   1GB
Nov 15 01:20:29 Starting compiler/parsing/tests
Nov 15 01:21:36 Finished compiler/parsing/tests                                1m06s 647MB
Nov 15 01:21:37 Starting compiler/inference/tests
Nov 15 01:38:10 Finished compiler/inference/tests                             16m33s   6GB
Nov 15 01:38:11 Starting compiler/printing/test
Nov 15 01:45:11 Finished compiler/printing/test                                7m00s   3GB
Nov 15 01:45:11 Starting floatingPoint/tools/flover
Nov 15 02:51:37 Finished floatingPoint/tools/flover                         1h06m25s   1GB
Nov 15 02:51:38 Starting floatingPoint/icing/
Nov 15 03:52:31 FAILED: floatingPoint/icing/
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/src/quotient/src[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/basis[0m
Scanning [1m$(HOLDIR)/examples/algorithms[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(HOLDIR)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/real[0m
Scanning [1m$(HOLDIR)/src/floating-point[0m
Scanning [1m$(HOLDIR)/src/monad/more_monads[0m
Scanning [1m$(HOLDIR)/src/update[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/ag32[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[0m
Scanning [1m$(HOLDIR)/examples/machine-code/decompiler[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm7[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm7[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm8[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/mips[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/mips[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/riscv[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/riscv[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/compiler[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/gc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/semantics/alt_semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/alt_semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/proofs[0m
Scanning [1m$(CAKEMLDIR)/floatingPoint/tools/flover/Infra[0m
Scanning [1m$(CAKEMLDIR)/floatingPoint/tools/flover/semantics[0m
Scanning [1m$(CAKEMLDIR)/floatingPoint/tools/flover[0m
Scanning [1m$(CAKEMLDIR)/unverified/sexpr-bootstrap[0m
Scanned 83 directories
Starting work on CakeMLtoFloVerTheory
Starting work on floatToRealTheory
Starting work on pureExpsTheory
Starting work on icing_optimisationsTheory
floatToRealTheory                                                                                                                                                                                    (18s)     OK
Starting work on README.md
README.md                                                                                                                                                                                             (0s)     OK
icing_optimisationsTheory                                                                                                                                                                            (21s)     OK
pureExpsTheory                                                                                                                                                                                       (71s)     OK
Starting work on icing_rewriterTheory
CakeMLtoFloVerTheory                                                                                                                                                                                 (78s)     OK
Starting work on CakeMLtoFloVerLemsTheory
icing_rewriterTheory                                                                                                                                                                                 (32s)     OK
Starting work on source_to_source2Theory
source_to_source2Theory                                                                                                                                                                              (35s)     OK
Starting work on icing_rewriterProofsTheory
Starting work on optPlannerTheory
optPlannerTheory                                                                                                                                                                                     (34s)     OK
icing_rewriterProofsTheory                                                                                                                                                                          (257s)     OK
Starting work on floatToRealProofsTheory
floatToRealProofsTheory                                                                                                                                                                              (76s)     OK
Starting work on source_to_source2ProofsTheory
CakeMLtoFloVerLemsTheory                                                                                                                                                                            (507s)     OK
Starting work on CakeMLtoFloVerProofsTheory
source_to_source2ProofsTheory                                                                                                                                                                       (416s)     OK
Starting work on icing_optimisationProofsTheory
CakeMLtoFloVerProofsTheory                                                                                                                                                                          (423s)     OK
Starting work on cfSupportTheory
icing_optimisationProofsTheory                                                                                                                                                                       (42m)     OK
Starting work on icing_realIdProofsTheory
Starting work on pull_wordsTheory
icing_realIdProofsTheory                                                                                                                                                                            (152s)     OK
Starting work on optPlannerProofsTheory
pull_wordsTheory                                                                                                                                                                                    (160s)FAIL<1>
 op a1 a2 refs1 refs2 ffi.
   LIST_REL v_rel a1 a2  LIST_REL ref_rel refs1 refs2 
   OPTREL
     (((r1,f1),v1) ((r2,f2),v2).
          f1 = f2  res1_rel v1 v2  LIST_REL ref_rel r1 r2)
     (do_app (refs1,ffi) op a1) (do_app (refs2,ffi) op a2)
 
 failed.
 Failed to prove theorem do_app_thm.
 Uncaught exception: HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 1327)", origin_function = "THEN1", origin_structure = "Tactical"}
optPlannerProofsTheory                                                                                                                                                                                (7s)MKILLED
cfSupportTheory                                                                                                                                                                                      (42m)MKILLED