05-30-01-23-default-1100-100.log

2024-05-30 01:23:36.378 | INFO     | __main__:main:291 - PID: 2742663
2024-05-30 01:23:36.378 | INFO     | __main__:main:292 - Namespace(data_path='data/leandojo_benchmark_4/random/', exp_id=None, split='test', file_path=None, full_name=None, name_filter=None, num_theorems=100, ckpt_path='/localscratch/hsun409/github/RiR/ckpts/leandojo-pl-ckpts/generator_random.ckpt', indexed_corpus_path=None, tactic=None, module=None, num_sampled_tactics=64, timeout=600, num_workers=4, num_gpus=4, verbose=False, start_ind=1100, gen_type='default')
2024-05-30 01:23:45.197 | INFO     | __main__:_get_theorems_from_files:121 - Starting from 1100th theorem named CommGroup.toGroup_injective!
2024-05-30 01:23:45.198 | INFO     | __main__:_get_theorems_from_files:127 - 100 theorems loaded from data/leandojo_benchmark_4/random/
2024-05-30 01:23:45.204 | INFO     | prover.proof_search:__init__:515 - Launching 4 workers with 4 GPUs.
2024-05-30 03:58:52.041 | INFO     | __main__:evaluate:199 - Evaluation done! 52 theorems proved, 47 theorems failed, 1 non-theorems discarded
2024-05-30 03:58:52.067 | INFO     | __main__:evaluate:214 - Results saved to ./results/default/80b14a3f-e586-4ba7-a39d-646e49113996_results.pickle
2024-05-30 03:58:52.070 | INFO     | __main__:main:315 - Pass@1: 0.5252525252525253