200000 playouts remaining SUCCESS Extension: [#,-l1_pre_topc(1^[])] Extension: [l1_pre_topc(1^[]),m1_pre_topc(2^[],1^[]),-m1_subset_1(u1_struct_0(2^[]),k1_zfmisc_1(u1_struct_0(1^[])))] Extension: [-m1_pre_topc(2^[],1^[]),#] Reduction: - # Extension: [m1_subset_1(u1_struct_0(2^[]),k1_zfmisc_1(u1_struct_0(1^[]))),#] Reduction: - # 199000 playouts remaining Moving root from 0 to 1 198000 playouts remaining 197000 playouts remaining Moving root from 1 to 2 196000 playouts remaining 195000 playouts remaining Moving root from 2 to 3 194000 playouts remaining 193000 playouts remaining Moving root from 3 to 4 192000 playouts remaining 191000 playouts remaining Unable to move root from 4, returning to the beginning 190000 playouts remaining SUCCESS Extension: [#,m1_subset_1(u1_struct_0(2^[]),k1_zfmisc_1(u1_struct_0(1^[])))] Extension: [-m1_subset_1(u1_struct_0(2^[]),k1_zfmisc_1(u1_struct_0(1^[]))),l1_pre_topc(1^[]),m1_pre_topc(2^[],1^[])] Extension: [-l1_pre_topc(1^[]),#] Reduction: - # Extension: [-m1_pre_topc(2^[],1^[]),#] Reduction: - # 189000 playouts remaining Moving root from 0 to 8 188000 playouts remaining 187000 playouts remaining Moving root from 8 to 9 186000 playouts remaining 185000 playouts remaining Moving root from 9 to 10 184000 playouts remaining 183000 playouts remaining Moving root from 10 to 11 182000 playouts remaining 181000 playouts remaining Unable to move root from 11, returning to the beginning SUCCESS Extension: [#,-m1_pre_topc(2^[],1^[])] Extension: [m1_pre_topc(2^[],1^[]),l1_pre_topc(1^[]),-m1_subset_1(u1_struct_0(2^[]),k1_zfmisc_1(u1_struct_0(1^[])))] Extension: [-l1_pre_topc(1^[]),#] Reduction: - # Extension: [m1_subset_1(u1_struct_0(2^[]),k1_zfmisc_1(u1_struct_0(1^[]))),#] Reduction: - # 180000 playouts remaining 179000 playouts remaining Moving root from 0 to 5 178000 playouts remaining 177000 playouts remaining Moving root from 5 to 6 176000 playouts remaining 175000 playouts remaining Moving root from 6 to 7 174000 playouts remaining 173000 playouts remaining Moving root from 7 to 12 172000 playouts remaining 171000 playouts remaining Unable to move root from 12, returning to the beginning 170000 playouts remaining 169000 playouts remaining Moving root from 0 to 8 168000 playouts remaining 167000 playouts remaining Moving root from 8 to 9 166000 playouts remaining 165000 playouts remaining Moving root from 9 to 10 164000 playouts remaining 163000 playouts remaining Moving root from 10 to 11 162000 playouts remaining 161000 playouts remaining Unable to move root from 11, returning to the beginning 160000 playouts remaining 159000 playouts remaining Moving root from 0 to 1 158000 playouts remaining 157000 playouts remaining Moving root from 1 to 2 156000 playouts remaining 155000 playouts remaining Moving root from 2 to 3 154000 playouts remaining 153000 playouts remaining Moving root from 3 to 4 152000 playouts remaining 151000 playouts remaining Unable to move root from 4, returning to the beginning 150000 playouts remaining 149000 playouts remaining Moving root from 0 to 5 148000 playouts remaining 147000 playouts remaining Moving root from 5 to 6 146000 playouts remaining 145000 playouts remaining Moving root from 6 to 7 144000 playouts remaining 143000 playouts remaining Moving root from 7 to 12 142000 playouts remaining 141000 playouts remaining Unable to move root from 12, returning to the beginning 140000 playouts remaining 139000 playouts remaining Moving root from 0 to 8 138000 playouts remaining 137000 playouts remaining Moving root from 8 to 9 136000 playouts remaining 135000 playouts remaining Moving root from 9 to 10 134000 playouts remaining 133000 playouts remaining Moving root from 10 to 11 132000 playouts remaining 131000 playouts remaining Unable to move root from 11, returning to the beginning 130000 playouts remaining 129000 playouts remaining Moving root from 0 to 5 128000 playouts remaining 127000 playouts remaining Moving root from 5 to 6 126000 playouts remaining 125000 playouts remaining Moving root from 6 to 7 124000 playouts remaining 123000 playouts remaining Moving root from 7 to 12 122000 playouts remaining 121000 playouts remaining Unable to move root from 12, returning to the beginning 120000 playouts remaining 119000 playouts remaining Moving root from 0 to 1 118000 playouts remaining 117000 playouts remaining Moving root from 1 to 2 116000 playouts remaining 115000 playouts remaining Moving root from 2 to 3 114000 playouts remaining 113000 playouts remaining Moving root from 3 to 4 112000 playouts remaining 111000 playouts remaining Unable to move root from 4, returning to the beginning 110000 playouts remaining 109000 playouts remaining Moving root from 0 to 5 108000 playouts remaining 107000 playouts remaining Moving root from 5 to 6 106000 playouts remaining 105000 playouts remaining Moving root from 6 to 7 104000 playouts remaining 103000 playouts remaining Moving root from 7 to 12 102000 playouts remaining 101000 playouts remaining Unable to move root from 12, returning to the beginning 100000 playouts remaining 99000 playouts remaining Moving root from 0 to 8 98000 playouts remaining 97000 playouts remaining Moving root from 8 to 9 96000 playouts remaining 95000 playouts remaining Moving root from 9 to 10 94000 playouts remaining 93000 playouts remaining Moving root from 10 to 11 92000 playouts remaining 91000 playouts remaining Unable to move root from 11, returning to the beginning 90000 playouts remaining 89000 playouts remaining Moving root from 0 to 1 88000 playouts remaining 87000 playouts remaining Moving root from 1 to 2 86000 playouts remaining 85000 playouts remaining Moving root from 2 to 3 84000 playouts remaining 83000 playouts remaining Moving root from 3 to 4 82000 playouts remaining 81000 playouts remaining Unable to move root from 4, returning to the beginning 80000 playouts remaining 79000 playouts remaining Moving root from 0 to 5 78000 playouts remaining 77000 playouts remaining Moving root from 5 to 6 76000 playouts remaining 75000 playouts remaining Moving root from 6 to 7 74000 playouts remaining 73000 playouts remaining Moving root from 7 to 12 72000 playouts remaining 71000 playouts remaining Unable to move root from 12, returning to the beginning 70000 playouts remaining 69000 playouts remaining Moving root from 0 to 1 68000 playouts remaining 67000 playouts remaining Moving root from 1 to 2 66000 playouts remaining 65000 playouts remaining Moving root from 2 to 3 64000 playouts remaining 63000 playouts remaining Moving root from 3 to 4 62000 playouts remaining 61000 playouts remaining Unable to move root from 4, returning to the beginning 60000 playouts remaining 59000 playouts remaining Moving root from 0 to 8 58000 playouts remaining 57000 playouts remaining Moving root from 8 to 9 56000 playouts remaining 55000 playouts remaining Moving root from 9 to 10 54000 playouts remaining 53000 playouts remaining Moving root from 10 to 11 52000 playouts remaining 51000 playouts remaining Unable to move root from 11, returning to the beginning 50000 playouts remaining 49000 playouts remaining Moving root from 0 to 1 48000 playouts remaining 47000 playouts remaining Moving root from 1 to 2 46000 playouts remaining 45000 playouts remaining Moving root from 2 to 3 44000 playouts remaining 43000 playouts remaining Moving root from 3 to 4 42000 playouts remaining 41000 playouts remaining Unable to move root from 4, returning to the beginning 40000 playouts remaining 39000 playouts remaining Moving root from 0 to 8 38000 playouts remaining 37000 playouts remaining Moving root from 8 to 9 36000 playouts remaining 35000 playouts remaining Moving root from 9 to 10 34000 playouts remaining 33000 playouts remaining Moving root from 10 to 11 32000 playouts remaining 31000 playouts remaining Unable to move root from 11, returning to the beginning 30000 playouts remaining 29000 playouts remaining Moving root from 0 to 5 28000 playouts remaining 27000 playouts remaining Moving root from 5 to 6 26000 playouts remaining 25000 playouts remaining Moving root from 6 to 7 24000 playouts remaining 23000 playouts remaining Moving root from 7 to 12 22000 playouts remaining 21000 playouts remaining Unable to move root from 12, returning to the beginning 20000 playouts remaining 19000 playouts remaining Moving root from 0 to 1 18000 playouts remaining 17000 playouts remaining Moving root from 1 to 2 16000 playouts remaining 15000 playouts remaining Moving root from 2 to 3 14000 playouts remaining 13000 playouts remaining Moving root from 3 to 4 12000 playouts remaining 11000 playouts remaining Unable to move root from 4, returning to the beginning 10000 playouts remaining 9000 playouts remaining Moving root from 0 to 8 8000 playouts remaining 7000 playouts remaining Moving root from 8 to 9 6000 playouts remaining 5000 playouts remaining Moving root from 9 to 10 4000 playouts remaining 3000 playouts remaining Moving root from 10 to 11 2000 playouts remaining 1000 playouts remaining Unable to move root from 11, returning to the beginning Created 13 nodes Bigstep Nodes: 13, [0,1,2,3,4,5,6,7,8,9,10,11,12] Training data collected Proof attempt leading to node 0: Prolog query: mc_run("theorems/m2np/l10_tex_2.p",[guided(0),cp(1),sim_depth(0),playout_count(200000),min_visit_count(1),n_dim(1009),playout_time(205), output_format(svmlight), leancop_settings([conj,nodef,comp(7)]),bigstep_frequency(2000)],"results/all/train_value","results/all/train_policy",ExecutionTime,InfToProofs) Problem theorems/m2np/l10_tex_2.p executed in 55.012 sec