PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-opt1217.opb
MD5SUM	697fa5beb3d240bccfa43a29ef9b4fb8
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-2048
Optimality of the best value was proved	NO
Number of terms in the objective function	16
Biggest coefficient in the objective function	32768
Number of bits for the biggest coefficient in the objective function	16
Sum of the numbers in the objective function	65535
Number of bits of the sum of numbers in the objective function	16
Biggest number in a constraint	49152
Number of bits of the biggest number in a constraint	16
Biggest sum of numbers in a constraint	114687
Number of bits of the biggest sum of numbers	17
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.03
Number of variables	784
Total number of constraints	833
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	816
Number of constraints which are nor clauses,nor cardinality constraints	17
Minimum length of a constraint	1
Maximum length of a constraint	64
Trace number 15358

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc13 THE 2005-04-21 04:02:05 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17874 boxname=wulflinc13 idbench=1375 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  697fa5beb3d240bccfa43a29ef9b4fb8  /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-opt1217.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-opt1217.opb /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-opt1217.opb
IDLAUNCH: 17874
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        811268 kB
Buffers:         33068 kB
Cached:         168444 kB
SwapCached:        176 kB
Active:          41548 kB
Inactive:       162684 kB
HighTotal:      131008 kB
HighFree:        23912 kB
LowTotal:       903652 kB
LowFree:        787356 kB
SwapTotal:     2097136 kB
SwapFree:      2096860 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6808 kB
Slab:            13516 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 04:22:08 (client local time) WITH STATUS 10 IN 1200.44 SECONDS
stats: 17874 7 1200.44 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 113 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 111]---> BDD-cost: 1469
c ---[ 110]---> BDD-cost: 1400
c ---[ 109]---> BDD-cost: 1650
c ---[ 108]---> BDD-cost: 1517
c ---[ 107]---> BDD-cost: 1701
c ---[ 106]---> BDD-cost: 1477
c ---[ 105]---> BDD-cost: 1174
c ---[ 104]---> BDD-cost:  883
c ---[ 102]---> BDD-cost:   29
c ---[ 100]---> BDD-cost:   29
c ---[  98]---> BDD-cost:   29
c ---[  97]---> BDD-cost: 1670
c ---[  95]---> BDD-cost:   29
c ---[  93]---> BDD-cost:   29
c ---[  91]---> BDD-cost:   29
c ---[  89]---> BDD-cost:   29
c ---[  87]---> BDD-cost:   29
c ---[  85]---> BDD-cost:   29
c ---[  83]---> BDD-cost:   29
c ---[  81]---> BDD-cost:   29
c ---[  79]---> BDD-cost:   29
c ---[  77]---> BDD-cost:   29
c ---[  76]---> BDD-cost: 1605
c ---[  74]---> BDD-cost:   29
c ---[  72]---> BDD-cost:   29
c ---[  70]---> BDD-cost:   29
c ---[  68]---> BDD-cost:   29
c ---[  66]---> BDD-cost:   29
c ---[  64]---> BDD-cost:   29
c ---[  62]---> BDD-cost:   29
c ---[  60]---> BDD-cost:   29
c ---[  58]---> BDD-cost:   29
c ---[  56]---> BDD-cost:   29
c ---[  55]---> BDD-cost: 1826
c ---[  53]---> BDD-cost:   29
c ---[  51]---> BDD-cost:   29
c ---[  49]---> BDD-cost:   29
c ---[  47]---> BDD-cost:   29
c ---[  45]---> BDD-cost:   29
c ---[  43]---> BDD-cost:   29
c ---[  41]---> BDD-cost:   29
c ---[  39]---> BDD-cost:   29
c ---[  37]---> BDD-cost:   29
c ---[  35]---> BDD-cost:   29
c ---[  34]---> BDD-cost: 1452
c ---[  32]---> BDD-cost:   29
c ---[  30]---> BDD-cost:   29
c ---[  28]---> BDD-cost:   29
c ---[  26]---> BDD-cost:   29
c ---[  24]---> BDD-cost:   29
c ---[  22]---> BDD-cost:   29
c ---[  20]---> BDD-cost:   29
c ---[  18]---> BDD-cost:   29
c ---[  16]---> BDD-cost:   29
c ---[  14]---> BDD-cost:   29
c ---[  13]---> BDD-cost: 1049
c ---[  11]---> BDD-cost:   29
c ---[   9]---> BDD-cost:   29
c ---[   7]---> BDD-cost:   29
c ---[   5]---> BDD-cost:   29
c ---[   3]---> BDD-cost:   29
c ---[   2]---> BDD-cost: 1962
c ---[   1]---> BDD-cost: 1619
c ---[   0]---> BDD-cost: 1856
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   72562   214428 |   24187       0        0     nan |  0.000 % |
c |       100 |   72562   214428 |   26605     100     9442    94.4 |  0.249 % |
c |       250 |   72562   214428 |   29266     250    19385    77.5 |  0.249 % |
c |       476 |   72562   214428 |   32192     476    30962    65.0 |  0.249 % |
c |       815 |   72562   214428 |   35412     815    41226    50.6 |  0.249 % |
c |      1321 |   72562   214428 |   38953    1321    70780    53.6 |  0.249 % |
c |      2081 |   72562   214428 |   42848    2081    93233    44.8 |  0.249 % |
c |      3221 |   72562   214428 |   47133    3221   187988    58.4 |  0.249 % |
c |      4929 |   72562   214428 |   51846    4929   386503    78.4 |  0.249 % |
c |      7491 |   72562   214428 |   57031    7491   671943    89.7 |  0.249 % |
c |     11336 |   72562   214428 |   62734   11336  1016720    89.7 |  0.249 % |
c ==============================================================================
c [1mFound solution: -512[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> Sorter-cost:   43     Base: 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11378 |   72627   214591 |   24209   11378  1017392    89.4 |  0.249 % |
c |     11479 |   72627   214591 |   26629   11479  1019749    88.8 |  0.253 % |
c |     11629 |   72627   214591 |   29292   11629  1024282    88.1 |  0.253 % |
c |     11856 |   72627   214591 |   32222   11856  1043039    88.0 |  0.253 % |
c |     12197 |   72627   214591 |   35444   12197  1061812    87.1 |  0.253 % |
c |     12703 |   72627   214591 |   38988   12703  1098044    86.4 |  0.253 % |
c |     13465 |   72627   214591 |   42887   13465  1153824    85.7 |  0.253 % |
c |     14605 |   72627   214591 |   47176   14605  1210667    82.9 |  0.253 % |
c |     16313 |   72627   214591 |   51894   16313  1365977    83.7 |  0.253 % |
c |     18877 |   72627   214591 |   57083   18877  1600263    84.8 |  0.253 % |
c |     22724 |   72627   214591 |   62791   22724  2076383    91.4 |  0.253 % |
c |     28490 |   72627   214591 |   69071   28490  2973036   104.4 |  0.253 % |
c |     37140 |   72627   214591 |   75978   37140  3162215    85.1 |  0.253 % |
c |     50120 |   72627   214591 |   83576   50120  5264951   105.0 |  0.253 % |
c |     69585 |   72627   214591 |   91933   69585  9389449   134.9 |  0.253 % |
c |     98777 |   72627   214591 |  101127   98777 14503682   146.8 |  0.253 % |
c |    142566 |   72627   214591 |  111239   54058  7134234   132.0 |  0.253 % |
c |    208251 |   72627   214591 |  122363  119743 17370785   145.1 |  0.253 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x1_bit_7 -x1_bit_6 -x1_bit_5 -x1_bit_4 -x1_bit_3 -x1_bit_2 -x1_bit_1 -x1_bit0 -x1_bit1 x1_bit2 -x1_bit3 -x1_bit4 -x1_bit5 -x1_bit6 -x1_bit7 -x1_bit8 -x2_bit0 -x3_bit0 -x4_bit0 -x5_bit0 -x6_bit0 -x7_bit0 -x8_bit0 -x9_bit0 -x10_bit0 -x11_bit0 -x12_bit0 -x13_bit0 -x14_bit0 -x15_bit0 -x16_bit0 x17_bit0 x18_bit0 -x19_bit0 -x20_bit0 -x21_bit0 -x22_bit0 -x23_bit0 -x24_bit0 -x25_bit0 -x26_bit0 -x27_bit0 x28_bit0 x29_bit0 -x30_bit0 -x31_bit0 -x32_bit0 -x33_bit0 -x34_bit0 -x35_bit0 -x36_bit0 -x37_bit0 -x38_bit0 -x39_bit0 -x40_bit0 -x41_bit0 -x42_bit0 -x43_bit0 -x44_bit0 -x45_bit0 -x46_bit0 -x47_bit0 -x48_bit0 -x49_bit0 -x50_bit0 -x51_bit0 -x52_bit0 -x53_bit0 -x54_bit0 -x55_bit0 -x56_bit0 -x57_bit0 -x58_bit0 -x59_bit0 -x60_bit0 -x61_bit0 -x62_bit0 -x63_bit0 -x64_bit0 -x65_bit0 -x66_bit0 x67_bit0 -x68_bit0 -x69_bit0 -x70_bit0 -x71_bit0 -x72_bit0 -x73_bit0 -x74_bit0 -x75_bit0 -x76_bit0 -x77_bit0 -x78_bit0 -x79_bit0 -x80_bit0 -x81_bit0 -x82_bit0 -x83_bit0 -x84_bit0 -x85_bit0 -x86_bit0 -x87_bit0 -x88_bit0 -x89_bit0 -x90_bit0 -x91_bit0 -x92_bit0 -x93_bit0 -x94_bit0 -x95_bit0 -x96_bit0 -x97_bit0 -x98_bit0 -x99_bit0 -x100_bit0 -x101_bit0 -x102_bit0 -x103_bit0 -x104_bit0 -x105_bit0 -x106_bit0 -x107_bit0 -x108_bit0 -x109_bit0 -x110_bit0 -x111_bit0 -x112_bit0 -x113_bit0 -x114_bit0 -x115_bit0 -x116_bit0 x117_bit0 -x118_bit0 -x119_bit0 -x120_bit0 -x121_bit0 -x122_bit0 -x123_bit0 -x124_bit0 -x125_bit0 -x126_bit0 -x127_bit0 -x128_bit0 x129_bit0 -x130_bit0 -x131_bit0 -x132_bit0 -x133_bit0 -x134_bit0 -x135_bit0 -x136_bit0 -x137_bit0 -x138_bit0 -x139_bit0 -x140_bit0 -x141_bit0 -x142_bit0 -x143_bit0 -x144_bit0 -x145_bit0 -x146_bit0 -x147_bit0 -x148_bit0 x149_bit0 -x150_bit0 x151_bit0 -x152_bit0 -x153_bit0 -x154_bit0 -x155_bit0 -x156_bit0 -x157_bit0 -x158_bit0 -x159_bit0 -x160_bit0 -x161_bit0 -x162_bit0 -x163_bit0 -x164_bit0 -x165_bit0 -x166_bit0 -x167_bit0 -x168_bit0 -x169_bit0 -x170_bit0 -x171_bit0 -x172_bit0 -x173_bit0 x174_bit0 x175_bit0 -x176_bit0 -x177_bit0 -x178_bit0 -x179_bit0 -x180_bit0 -x181_bit0 -x182_bit0 -x183_bit0 -x184_bit0 -x185_bit0 -x186_bit0 -x187_bit0 -x188_bit0 x189_bit0 -x190_bit0 x191_bit0 x192_bit0 -x193_bit0 -x194_bit0 -x195_bit0 x196_bit0 -x197_bit0 x198_bit0 -x199_bit0 x200_bit0 x201_bit0 -x202_bit0 -x203_bit0 -x204_bit0 -x205_bit0 -x206_bit0 -x207_bit0 -x208_bit0 -x209_bit0 -x210_bit0 x211_bit0 -x212_bit0 x213_bit0 x214_bit0 x215_bit0 -x216_bit0 x217_bit0 x218_bit0 -x219_bit0 -x220_bit0 x221_bit0 -x222_bit0 -x223_bit0 -x224_bit0 -x225_bit0 x226_bit0 -x227_bit0 -x228_bit0 -x229_bit0 -x230_bit0 -x231_bit0 -x232_bit0 x233_bit0 x234_bit0 x235_bit0 -x236_bit0 -x237_bit0 -x238_bit0 -x239_bit0 -x240_bit0 -x241_bit0 -x242_bit0 -x243_bit0 -x244_bit0 -x245_bit0 -x246_bit0 -x247_bit0 -x248_bit0 -x249_bit0 -x250_bit0 -x251_bit0 -x252_bit0 -x253_bit0 -x254_bit0 -x255_bit0 -x256_bit0 -x257_bit0 -x258_bit0 -x259_bit0 -x260_bit0 -x261_bit0 -x262_bit0 -x263_bit0 -x264_bit0 -x265_bit0 -x266_bit0 -x267_bit0 -x268_bit0 -x269_bit0 -x270_bit0 x271_bit0 -x272_bit0 -x273_bit0 -x274_bit0 -x275_bit0 -x276_bit0 -x277_bit0 -x278_bit0 -x279_bit0 -x280_bit0 -x281_bit0 -x282_bit0 -x283_bit0 -x284_bit0 x285_bit0 x286_bit0 -x287_bit0 -x288_bit0 -x289_bit0 -x290_bit0 -x291_bit0 -x292_bit0 -x293_bit0 x294_bit0 x295_bit0 -x296_bit0 x297_bit0 x298_bit0 -x299_bit0 -x300_bit0 -x301_bit0 -x302_bit0 -x303_bit0 -x304_bit0 -x305_bit0 -x306_bit0 -x307_bit0 -x308_bit0 -x309_bit0 -x310_bit0 -x311_bit0 -x312_bit0 -x313_bit0 -x314_bit0 -x315_bit0 -x316_bit0 -x317_bit0 -x318_bit0 -x319_bit0 x320_bit0 -x321_bit0 -x322_bit0 -x323_bit0 -x324_bit0 -x325_bit0 -x326_bit0 -x327_bit0 -x328_bit0 -x329_bit0 -x330_bit0 -x331_bit0 -x332_bit0 -x333_bit0 -x334_bit0 -x335_bit0 -x336_bit0 -x337_bit0 -x338_bit0 -x339_bit0 -x340_bit0 -x341_bit0 -x342_bit0 -x343_bit0 -x344_bit0 -x345_bit0 -x346_bit0 -x347_bit0 -x348_bit0 -x349_bit0 -x350_bit0 -x351_bit0 -x352_bit0 -x353_bit0 -x354_bit0 -x355_bit0 -x356_bit0 -x357_bit0 -x358_bit0 -x359_bit0 -x360_bit0 -x361_bit0 -x362_bit0 -x363_bit0 -x364_bit0 -x365_bit0 -x366_bit0 -x367_bit0 -x368_bit0 -x369_bit0 -x370_bit0 -x371_bit0 -x372_bit0 -x373_bit0 -x374_bit0 -x375_bit0 x376_bit0 -x377_bit0 -x378_bit0 -x379_bit0 -x380_bit0 -x381_bit0 -x382_bit0 -x383_bit0 -x384_bit0 -x385_bit0 -x386_bit0 -x387_bit0 -x388_bit0 -x389_bit0 -x390_bit0 -x391_bit0 -x392_bit0 -x393_bit0 -x394_bit0 -x395_bit0 -x396_bit0 -x397_bit0 -x398_bit0 -x399_bit0 -x400_bit0 -x401_bit0 -x402_bit0 -x403_bit0 -x404_bit0 -x405_bit0 -x406_bit0 -x407_bit0 -x408_bit0 -x409_bit0 -x410_bit0 -x411_bit0 -x412_bit0 -x413_bit0 -x414_bit0 -x415_bit0 -x416_bit0 -x417_bit0 -x418_bit0 -x419_bit0 x420_bit0 -x421_bit0 -x422_bit0 -x423_bit0 -x424_bit0 -x425_bit0 -x426_bit0 -x427_bit0 -x428_bit0 -x429_bit0 -x430_bit0 -x431_bit0 -x432_bit0 -x433_bit0 -x434_bit0 -x435_bit0 -x436_bit0 -x437_bit0 -x438_bit0 -x439_bit0 -x440_bit0 -x441_bit0 -x442_bit0 -x443_bit0 x444_bit0 -x445_bit0 -x446_bit0 -x447_bit0 -x448_bit0 -x449_bit0 -x450_bit0 -x451_bit0 -x452_bit0 -x453_bit0 -x454_bit0 -x455_bit0 -x456_bit0 -x457_bit0 -x458_bit0 -x459_bit0 -x460_bit0 -x461_bit0 -x462_bit0 -x463_bit0 -x464_bit0 -x465_bit0 -x466_bit0 -x467_bit0 -x468_bit0 -x469_bit0 -x470_bit0 -x471_bit0 -x472_bit0 -x473_bit0 -x474_bit0 -x475_bit0 -x476_bit0 -x477_bit0 -x478_bit0 -x479_bit0 -x480_bit0 -x481_bit0 -x482_bit0 -x483_bit0 -x484_bit0 -x485_bit0 -x486_bit0 -x487_bit0 -x488_bit0 -x489_bit0 -x490_bit0 -x491_bit0 -x492_bit0 -x493_bit0 -x494_bit0 -x495_bit0 -x496_bit0 -x497_bit0 -x498_bit0 -x499_bit0 -x500_bit0 -x501_bit0 -x502_bit0 -x503_bit0 -x504_bit0 -x505_bit0 -x506_bit0 -x507_bit0 -x508_bit0 -x509_bit0 -x510_bit0 -x511_bit0 -x512_bit0 -x513_bit0 -x514_bit0 -x515_bit0 -x516_bit0 -x517_bit0 -x518_bit0 -x519_bit0 x520_bit0 -x521_bit0 -x522_bit0 -x523_bit0 -x524_bit0 -x525_bit0 -x526_bit0 -x527_bit0 -x528_bit0 -x529_bit0 -x530_bit0 -x531_bit0 -x532_bit0 -x533_bit0 -x534_bit0 -x535_bit0 -x536_bit0 -x537_bit0 -x538_bit0 -x539_bit0 -x540_bit0 -x541_bit0 -x542_bit0 -x543_bit0 -x544_bit0 -x545_bit0 -x546_bit0 -x547_bit0 -x548_bit0 -x549_bit0 -x550_bit0 -x551_bit0 -x552_bit0 -x553_bit0 -x554_bit0 -x555_bit0 -x556_bit0 -x557_bit0 -x558_bit0 -x559_bit0 x560_bit0 -x561_bit0 -x562_bit0 -x563_bit0 -x564_bit0 -x565_bit0 -x566_bit0 -x567_bit0 -x568_bit0 -x569_bit0 -x570_bit0 -x571_bit0 -x572_bit0 -x573_bit0 -x574_bit0 -x575_bit0 -x576_bit0 -x577_bit0 -x578_bit0 -x579_bit0 -x580_bit0 -x581_bit0 x582_bit0 -x583_bit0 -x584_bit0 -x585_bit0 -x586_bit0 -x587_bit0 -x588_bit0 -x589_bit0 -x590_bit0 -x591_bit0 -x592_bit0 -x593_bit0 -x594_bit0 -x595_bit0 -x596_bit0 -x597_bit0 -x598_bit0 -x599_bit0 -x600_bit0 -x601_bit0 -x602_bit0 -x603_bit0 -x604_bit0 -x605_bit0 -x606_bit0 -x607_bit0 -x608_bit0 -x609_bit0 -x610_bit0 -x611_bit0 -x612_bit0 -x613_bit0 -x614_bit0 -x615_bit0 -x616_bit0 -x617_bit0 -x618_bit0 -x619_bit0 -x620_bit0 -x621_bit0 -x622_bit0 -x623_bit0 -x624_bit0 -x625_bit0 -x626_bit0 -x627_bit0 -x628_bit0 -x629_bit0 -x630_bit0 -x631_bit0 -x632_bit0 -x633_bit0 -x634_bit0 -x635_bit0 -x636_bit0 -x637_bit0 -x638_bit0 -x639_bit0 -x640_bit0 -x641_bit0 -x642_bit0 -x643_bit0 -x644_bit0 -x645_bit0 -x646_bit0 -x647_bit0 -x648_bit0 -x649_bit0 -x650_bit0 -x651_bit0 -x652_bit0 -x653_bit0 x654_bit0 -x655_bit0 x656_bit0 -x657_bit0 -x658_bit0 -x659_bit0 -x660_bit0 -x661_bit0 -x662_bit0 -x663_bit0 -x664_bit0 -x665_bit0 -x666_bit0 -x667_bit0 x668_bit0 -x669_bit0 -x670_bit0 -x671_bit0 -x672_bit0 -x673_bit0 -x674_bit0 -x675_bit0 -x676_bit0 -x677_bit0 -x678_bit0 -x679_bit0 -x680_bit0 -x681_bit0 -x682_bit0 -x683_bit0 -x684_bit0 -x685_bit0 -x686_bit0 -x687_bit0 -x688_bit0 -x689_bit0 -x690_bit0 -x691_bit0 -x692_bit0 -x693_bit0 -x694_bit0 -x695_bit0 -x696_bit0 -x697_bit0 -x698_bit0 -x699_bit0 -x700_bit0 -x701_bit0 -x702_bit0 -x703_bit0 -x704_bit0 -x705_bit0 -x706_bit0 -x707_bit0 -x708_bit0 -x709_bit0 -x710_bit0 -x711_bit0 -x712_bit0 -x713_bit0 -x714_bit0 -x715_bit0 -x716_bit0 -x717_bit0 -x718_bit0 -x719_bit0 -x720_bit0 -x721_bit0 -x722_bit0 -x723_bit0 -x724_bit0 -x725_bit0 -x726_bit0 -x727_bit0 -x728_bit0 -x729_bit0 -x730_bit0 -x731_bit0 -x732_bit0 -x733_bit0 -x734_bit0 -x735_bit0 x736_bit0 -x737_bit0 -x738_bit0 -x739_bit0 -x740_bit0 -x741_bit0 -x742_bit0 -x74#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.97 0.95 1/54 29572
Raw data (stat): 29572 (runsolver) R 29571 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 483825356 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.002 s]
Raw data (loadavg): 0.88 0.97 0.95 2/54 29572
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 2768 0 0 0 990 8 0 0 25 0 1 0 483825356 13340672 2688 4294967295 134512640 134672761 3221224528 3221223664 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3257 2688 603 41 0 3216 0
vsize: 13028
[startup+20.0028 s]
Raw data (loadavg): 0.89 0.97 0.95 2/54 29572
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 3225 0 0 0 1988 10 0 0 25 0 1 0 483825356 15228928 3145 4294967295 134512640 134672761 3221224528 3221223712 134558754 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3718 3145 603 41 0 3677 0
vsize: 14872
[startup+30.003 s]
Raw data (loadavg): 0.91 0.97 0.95 2/54 29572
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 3709 0 0 0 2986 12 0 0 25 0 1 0 483825356 17248256 3629 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4211 3629 603 41 0 4170 0
vsize: 16844
[startup+40.0041 s]
Raw data (loadavg): 0.92 0.97 0.95 2/54 29572
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 3962 0 0 0 3985 13 0 0 25 0 1 0 483825356 18223104 3882 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4449 3882 603 41 0 4408 0
vsize: 17796
[startup+50.0047 s]
Raw data (loadavg): 0.93 0.97 0.95 2/54 29572
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 4194 0 0 0 4985 14 0 0 25 0 1 0 483825356 19288064 4114 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4709 4114 603 41 0 4668 0
vsize: 18836
[startup+60.0044 s]
Raw data (loadavg): 0.94 0.97 0.95 2/54 29572
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 4389 0 0 0 5984 15 0 0 25 0 1 0 483825356 19959808 4309 4294967295 134512640 134672761 3221224528 3221223728 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4873 4309 603 41 0 4832 0
vsize: 19492
[startup+70.0086 s]
Raw data (loadavg): 0.95 0.97 0.95 2/54 29572
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 4670 0 0 0 6983 16 0 0 25 0 1 0 483825356 21176320 4590 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5170 4590 603 41 0 5129 0
vsize: 20680
[startup+80.0127 s]
Raw data (loadavg): 0.96 0.97 0.95 2/54 29572
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 4910 0 0 0 7983 17 0 0 25 0 1 0 483825356 22102016 4830 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5396 4830 603 41 0 5355 0
vsize: 21584
[startup+90.0129 s]
Raw data (loadavg): 0.97 0.97 0.95 2/54 29572
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 5303 0 0 0 8981 18 0 0 25 0 1 0 483825356 23719936 5223 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5791 5223 603 41 0 5750 0
vsize: 23164
[startup+100.013 s]
Raw data (loadavg): 0.97 0.97 0.95 2/54 29572
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 5724 0 0 0 9979 20 0 0 25 0 1 0 483825356 25468928 5644 4294967295 134512640 134672761 3221224528 3221223696 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6218 5644 603 41 0 6177 0
vsize: 24872
[startup+110.014 s]
Raw data (loadavg): 0.97 0.97 0.95 2/54 29572
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 5928 0 0 0 10978 21 0 0 25 0 1 0 483825356 26275840 5848 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6415 5848 603 41 0 6374 0
vsize: 25660
[startup+120.015 s]
Raw data (loadavg): 0.98 0.97 0.95 2/54 29572
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 6004 0 0 0 11978 21 0 0 25 0 1 0 483825356 26542080 5924 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6480 5924 603 41 0 6439 0
vsize: 25920
[startup+130.016 s]
Raw data (loadavg): 0.98 0.97 0.95 2/54 29572
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 6076 0 0 0 12978 22 0 0 25 0 1 0 483825356 26935296 5996 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6576 5996 603 41 0 6535 0
vsize: 26304
[startup+140.016 s]
Raw data (loadavg): 0.98 0.97 0.95 2/54 29572
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 6287 0 0 0 13976 23 0 0 25 0 1 0 483825356 27877376 6207 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6806 6207 603 41 0 6765 0
vsize: 27224
[startup+150.016 s]
Raw data (loadavg): 0.98 0.97 0.95 2/54 29572
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 6765 0 0 0 14975 25 0 0 25 0 1 0 483825356 29757440 6685 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7265 6685 603 41 0 7224 0
vsize: 29060
[startup+160.016 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29572
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 7201 0 0 0 15973 27 0 0 25 0 1 0 483825356 31641600 7121 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7725 7121 603 41 0 7684 0
vsize: 30900
[startup+170.017 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29572
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 7604 0 0 0 16972 28 0 0 25 0 1 0 483825356 33239040 7524 4294967295 134512640 134672761 3221224528 3221223664 134560590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8115 7524 603 41 0 8074 0
vsize: 32460
[startup+180.018 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29572
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 8036 0 0 0 17970 30 0 0 25 0 1 0 483825356 34988032 7956 4294967295 134512640 134672761 3221224528 3221223664 134560566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8542 7956 603 41 0 8501 0
vsize: 34168
[startup+190.018 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 8449 0 0 0 18968 32 0 0 25 0 1 0 483825356 36605952 8369 4294967295 134512640 134672761 3221224528 3221223696 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8937 8369 603 41 0 8896 0
vsize: 35748
[startup+200.019 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 8770 0 0 0 19967 33 0 0 25 0 1 0 483825356 37957632 8690 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9267 8690 603 41 0 9226 0
vsize: 37068
[startup+210.018 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 9120 0 0 0 20967 34 0 0 25 0 1 0 483825356 39436288 9040 4294967295 134512640 134672761 3221224528 3221223712 134559663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9628 9040 603 41 0 9587 0
vsize: 38512
[startup+220.019 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 9491 0 0 0 21965 35 0 0 25 0 1 0 483825356 40923136 9411 4294967295 134512640 134672761 3221224528 3221223696 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9991 9411 603 41 0 9950 0
vsize: 39964
[startup+230.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 9909 0 0 0 22964 37 0 0 25 0 1 0 483825356 42676224 9829 4294967295 134512640 134672761 3221224528 3221223632 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10419 9829 603 41 0 10378 0
vsize: 41676
[startup+240.019 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 10281 0 0 0 23963 38 0 0 25 0 1 0 483825356 44146688 10201 4294967295 134512640 134672761 3221224528 3221223632 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10778 10201 603 41 0 10737 0
vsize: 43112
[startup+250.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 10681 0 0 0 24960 41 0 0 25 0 1 0 483825356 45760512 10601 4294967295 134512640 134672761 3221224528 3221223696 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11172 10601 603 41 0 11131 0
vsize: 44688
[startup+260.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 11079 0 0 0 25959 42 0 0 25 0 1 0 483825356 47484928 10999 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11593 10999 603 41 0 11552 0
vsize: 46372
[startup+270.021 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 11512 0 0 0 26958 43 0 0 25 0 1 0 483825356 49221632 11432 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12017 11432 603 41 0 11976 0
vsize: 48068
[startup+280.021 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 11966 0 0 0 27957 44 0 0 25 0 1 0 483825356 51363840 11886 4294967295 134512640 134672761 3221224528 3221223632 134559866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12540 11886 603 41 0 12499 0
vsize: 50160
[startup+290.021 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 12412 0 0 0 28955 46 0 0 25 0 1 0 483825356 53121024 12332 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12969 12332 603 41 0 12928 0
vsize: 51876
[startup+300.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 12909 0 0 0 29954 47 0 0 25 0 1 0 483825356 55144448 12829 4294967295 134512640 134672761 3221224528 3221223696 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13463 12829 603 41 0 13422 0
vsize: 53852
[startup+310.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 13232 0 0 0 30954 48 0 0 25 0 1 0 483825356 56483840 13152 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13790 13152 603 41 0 13749 0
vsize: 55160
[startup+320.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 13609 0 0 0 31953 48 0 0 25 0 1 0 483825356 57978880 13529 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14155 13529 603 41 0 14114 0
vsize: 56620
[startup+330.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 14007 0 0 0 32952 49 0 0 25 0 1 0 483825356 59584512 13927 4294967295 134512640 134672761 3221224528 3221223664 134560726 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14547 13927 603 41 0 14506 0
vsize: 58188
[startup+340.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 14337 0 0 0 33952 50 0 0 25 0 1 0 483825356 60932096 14257 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14876 14257 603 41 0 14835 0
vsize: 59504
[startup+350.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 14708 0 0 0 34951 52 0 0 25 0 1 0 483825356 62418944 14628 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15239 14628 603 41 0 15198 0
vsize: 60956
[startup+360.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 15098 0 0 0 35950 53 0 0 25 0 1 0 483825356 64036864 15018 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15634 15018 603 41 0 15593 0
vsize: 62536
[startup+370.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 15469 0 0 0 36949 53 0 0 25 0 1 0 483825356 65523712 15389 4294967295 134512640 134672761 3221224528 3221223696 134561220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15997 15389 603 41 0 15956 0
vsize: 63988
[startup+380.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 15880 0 0 0 37948 55 0 0 25 0 1 0 483825356 67260416 15800 4294967295 134512640 134672761 3221224528 3221223696 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16421 15800 603 41 0 16380 0
vsize: 65684
[startup+390.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 16267 0 0 0 38948 55 0 0 25 0 1 0 483825356 68866048 16187 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16813 16187 603 41 0 16772 0
vsize: 67252
[startup+400.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 16666 0 0 0 39947 57 0 0 25 0 1 0 483825356 70479872 16586 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17207 16586 603 41 0 17166 0
vsize: 68828
[startup+410.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 17058 0 0 0 40946 57 0 0 25 0 1 0 483825356 72093696 16978 4294967295 134512640 134672761 3221224528 3221223632 134560169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17601 16979 603 41 0 17560 0
vsize: 70404
[startup+420.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 17491 0 0 0 41945 58 0 0 25 0 1 0 483825356 73826304 17411 4294967295 134512640 134672761 3221224528 3221223632 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18024 17411 603 41 0 17983 0
vsize: 72096
[startup+430.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 17885 0 0 0 42945 59 0 0 25 0 1 0 483825356 75431936 17805 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18416 17805 603 41 0 18375 0
vsize: 73664
[startup+440.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 18183 0 0 0 43944 60 0 0 25 0 1 0 483825356 76640256 18103 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18711 18103 603 41 0 18670 0
vsize: 74844
[startup+450.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 18439 0 0 0 44943 61 0 0 25 0 1 0 483825356 77709312 18359 4294967295 134512640 134672761 3221224528 3221223696 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18972 18359 603 41 0 18931 0
vsize: 75888
[startup+460.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 18601 0 0 0 45943 61 0 0 25 0 1 0 483825356 78381056 18521 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19136 18521 603 41 0 19095 0
vsize: 76544
[startup+470.032 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 18601 0 0 0 46944 61 0 0 25 0 1 0 483825356 78381056 18521 4294967295 134512640 134672761 3221224528 3221223696 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19136 18521 603 41 0 19095 0
vsize: 76544
[startup+480.034 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 18601 0 0 0 47944 61 0 0 25 0 1 0 483825356 78381056 18521 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19136 18521 603 41 0 19095 0
vsize: 76544
[startup+490.033 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 18601 0 0 0 48944 61 0 0 25 0 1 0 483825356 78381056 18521 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19136 18521 603 41 0 19095 0
vsize: 76544
[startup+500.042 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 18601 0 0 0 49945 61 0 0 25 0 1 0 483825356 78381056 18521 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19136 18521 603 41 0 19095 0
vsize: 76544
[startup+510.043 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 18601 0 0 0 50945 61 0 0 25 0 1 0 483825356 78381056 18521 4294967295 134512640 134672761 3221224528 3221223664 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19136 18521 603 41 0 19095 0
vsize: 76544
[startup+520.043 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 18601 0 0 0 51946 61 0 0 25 0 1 0 483825356 78381056 18521 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19136 18521 603 41 0 19095 0
vsize: 76544
[startup+530.043 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 18601 0 0 0 52946 61 0 0 25 0 1 0 483825356 78381056 18521 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19136 18521 603 41 0 19095 0
vsize: 76544
[startup+540.045 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 18601 0 0 0 53946 61 0 0 25 0 1 0 483825356 78381056 18521 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19136 18521 603 41 0 19095 0
vsize: 76544
[startup+550.045 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 18601 0 0 0 54946 61 0 0 25 0 1 0 483825356 78381056 18521 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19136 18521 603 41 0 19095 0
vsize: 76544
[startup+560.064 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 18601 0 0 0 55948 61 0 0 25 0 1 0 483825356 78381056 18521 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19136 18521 603 41 0 19095 0
vsize: 76544
[startup+570.093 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 18601 0 0 0 56952 61 0 0 25 0 1 0 483825356 78381056 18521 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19136 18521 603 41 0 19095 0
vsize: 76544
[startup+580.093 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 18601 0 0 0 57952 61 0 0 25 0 1 0 483825356 78381056 18521 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19136 18521 603 41 0 19095 0
vsize: 76544
[startup+590.096 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 18601 0 0 0 58952 61 0 0 25 0 1 0 483825356 78381056 18521 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19136 18521 603 41 0 19095 0
vsize: 76544
[startup+600.155 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 18601 0 0 0 59958 61 0 0 25 0 1 0 483825356 78381056 18521 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19136 18521 603 41 0 19095 0
vsize: 76544
[startup+610.205 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 18601 0 0 0 60963 61 0 0 25 0 1 0 483825356 78381056 18521 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19136 18521 603 41 0 19095 0
vsize: 76544
[startup+620.206 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 18601 0 0 0 61963 61 0 0 25 0 1 0 483825356 78381056 18521 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19136 18521 603 41 0 19095 0
vsize: 76544
[startup+630.207 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 18601 0 0 0 62962 62 0 0 25 0 1 0 483825356 78381056 18521 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19136 18521 603 41 0 19095 0
vsize: 76544
[startup+640.207 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 18601 0 0 0 63962 62 0 0 25 0 1 0 483825356 78381056 18521 4294967295 134512640 134672761 3221224528 3221223652 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19136 18521 603 41 0 19095 0
vsize: 76544
[startup+650.207 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 18601 0 0 0 64962 62 0 0 25 0 1 0 483825356 78381056 18521 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19136 18521 603 41 0 19095 0
vsize: 76544
[startup+660.213 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 18601 0 0 0 65962 63 0 0 25 0 1 0 483825356 78381056 18521 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19136 18521 603 41 0 19095 0
vsize: 76544
[startup+670.214 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 18601 0 0 0 66961 63 0 0 25 0 1 0 483825356 78381056 18521 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19136 18521 603 41 0 19095 0
vsize: 76544
[startup+680.224 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 18601 0 0 0 67962 63 0 0 25 0 1 0 483825356 78381056 18521 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19136 18521 603 41 0 19095 0
vsize: 76544
[startup+690.223 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 18601 0 0 0 68962 63 0 0 25 0 1 0 483825356 78381056 18521 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19136 18521 603 41 0 19095 0
vsize: 76544
[startup+700.224 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 18602 0 0 0 69963 63 0 0 25 0 1 0 483825356 78381056 18522 4294967295 134512640 134672761 3221224528 3221223632 134560184 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19136 18522 603 41 0 19095 0
vsize: 76544
[startup+710.223 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 18602 0 0 0 70963 63 0 0 25 0 1 0 483825356 78381056 18522 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19136 18522 603 41 0 19095 0
vsize: 76544
[startup+720.224 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 18602 0 0 0 71963 63 0 0 25 0 1 0 483825356 78381056 18522 4294967295 134512640 134672761 3221224528 3221223632 134560212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19136 18522 603 41 0 19095 0
vsize: 76544
[startup+730.224 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 18602 0 0 0 72963 63 0 0 25 0 1 0 483825356 78381056 18522 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19136 18522 603 41 0 19095 0
vsize: 76544
[startup+740.223 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 18602 0 0 0 73963 63 0 0 25 0 1 0 483825356 78381056 18522 4294967295 134512640 134672761 3221224528 3221223712 134558537 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19136 18522 603 41 0 19095 0
vsize: 76544
[startup+750.226 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 18602 0 0 0 74964 63 0 0 25 0 1 0 483825356 78381056 18522 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19136 18522 603 41 0 19095 0
vsize: 76544
[startup+760.226 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 18602 0 0 0 75964 63 0 0 25 0 1 0 483825356 78381056 18522 4294967295 134512640 134672761 3221224528 3221223696 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19136 18522 603 41 0 19095 0
vsize: 76544
[startup+770.225 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 18602 0 0 0 76964 63 0 0 25 0 1 0 483825356 78381056 18522 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19136 18522 603 41 0 19095 0
vsize: 76544
[startup+780.226 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 18602 0 0 0 77964 63 0 0 25 0 1 0 483825356 78381056 18522 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19136 18522 603 41 0 19095 0
vsize: 76544
[startup+790.225 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 18602 0 0 0 78964 63 0 0 25 0 1 0 483825356 78381056 18522 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19136 18522 603 41 0 19095 0
vsize: 76544
[startup+800.224 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 18602 0 0 0 79964 63 0 0 25 0 1 0 483825356 78381056 18522 4294967295 134512640 134672761 3221224528 3221223632 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19136 18522 603 41 0 19095 0
vsize: 76544
[startup+810.241 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 18603 0 0 0 80966 63 0 0 25 0 1 0 483825356 78381056 18523 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19136 18523 603 41 0 19095 0
vsize: 76544
[startup+820.259 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 18603 0 0 0 81968 63 0 0 25 0 1 0 483825356 78381056 18523 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19136 18523 603 41 0 19095 0
vsize: 76544
[startup+830.258 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 18603 0 0 0 82968 63 0 0 25 0 1 0 483825356 78381056 18523 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19136 18523 603 41 0 19095 0
vsize: 76544
[startup+840.265 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 18603 0 0 0 83969 63 0 0 25 0 1 0 483825356 78381056 18523 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19136 18523 603 41 0 19095 0
vsize: 76544
[startup+850.265 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 18603 0 0 0 84969 63 0 0 25 0 1 0 483825356 78381056 18523 4294967295 134512640 134672761 3221224528 3221223600 134541850 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19136 18523 603 41 0 19095 0
vsize: 76544
[startup+860.264 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 18717 0 0 0 85969 64 0 0 25 0 1 0 483825356 78782464 18637 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19234 18637 603 41 0 19193 0
vsize: 76936
[startup+870.264 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 19133 0 0 0 86968 65 0 0 25 0 1 0 483825356 80539648 19053 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19663 19053 603 41 0 19622 0
vsize: 78652
[startup+880.264 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 19507 0 0 0 87967 66 0 0 25 0 1 0 483825356 82022400 19427 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20025 19427 603 41 0 19984 0
vsize: 80100
[startup+890.263 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 19821 0 0 0 88966 67 0 0 25 0 1 0 483825356 83369984 19741 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20354 19741 603 41 0 20313 0
vsize: 81416
[startup+900.264 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 20160 0 0 0 89965 68 0 0 25 0 1 0 483825356 84717568 20080 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20683 20080 603 41 0 20642 0
vsize: 82732
[startup+910.263 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 20505 0 0 0 90965 69 0 0 25 0 1 0 483825356 86200320 20425 4294967295 134512640 134672761 3221224528 3221223664 134560675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21045 20425 603 41 0 21004 0
vsize: 84180
[startup+920.263 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 20842 0 0 0 91964 70 0 0 25 0 1 0 483825356 87539712 20762 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21372 20762 603 41 0 21331 0
vsize: 85488
[startup+930.263 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 21186 0 0 0 92963 71 0 0 25 0 1 0 483825356 88883200 21106 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21700 21106 603 41 0 21659 0
vsize: 86800
[startup+940.263 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 21512 0 0 0 93962 72 0 0 25 0 1 0 483825356 90222592 21432 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22027 21432 603 41 0 21986 0
vsize: 88108
[startup+950.262 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 21860 0 0 0 94962 72 0 0 25 0 1 0 483825356 91697152 21780 4294967295 134512640 134672761 3221224528 3221223632 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22387 21780 603 41 0 22346 0
vsize: 89548
[startup+960.263 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 21979 0 0 0 95961 73 0 0 25 0 1 0 483825356 92233728 21899 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22518 21899 603 41 0 22477 0
vsize: 90072
[startup+970.263 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 22056 0 0 0 96961 73 0 0 25 0 1 0 483825356 92499968 21976 4294967295 134512640 134672761 3221224528 3221223672 134560553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22583 21976 603 41 0 22542 0
vsize: 90332
[startup+980.262 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 22146 0 0 0 97961 74 0 0 25 0 1 0 483825356 92897280 22066 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22680 22066 603 41 0 22639 0
vsize: 90720
[startup+990.262 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 22154 0 0 0 98961 74 0 0 25 0 1 0 483825356 92897280 22074 4294967295 134512640 134672761 3221224528 3221223632 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22680 22074 603 41 0 22639 0
vsize: 90720
[startup+1000.26 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 22154 0 0 0 99961 74 0 0 25 0 1 0 483825356 92897280 22074 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22680 22074 603 41 0 22639 0
vsize: 90720
[startup+1010.26 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 22154 0 0 0 100961 74 0 0 25 0 1 0 483825356 92897280 22074 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22680 22074 603 41 0 22639 0
vsize: 90720
[startup+1020.26 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 22154 0 0 0 101961 74 0 0 25 0 1 0 483825356 92897280 22074 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22680 22074 603 41 0 22639 0
vsize: 90720
[startup+1030.26 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 22154 0 0 0 102961 74 0 0 25 0 1 0 483825356 92897280 22074 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22680 22074 603 41 0 22639 0
vsize: 90720
[startup+1040.26 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 22154 0 0 0 103962 74 0 0 25 0 1 0 483825356 92897280 22074 4294967295 134512640 134672761 3221224528 3221223696 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22680 22074 603 41 0 22639 0
vsize: 90720
[startup+1050.26 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 22154 0 0 0 104962 74 0 0 25 0 1 0 483825356 92897280 22074 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22680 22074 603 41 0 22639 0
vsize: 90720
[startup+1060.26 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 22154 0 0 0 105962 74 0 0 25 0 1 0 483825356 92897280 22074 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22680 22074 603 41 0 22639 0
vsize: 90720
[startup+1070.26 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 22154 0 0 0 106962 74 0 0 25 0 1 0 483825356 92897280 22074 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22680 22074 603 41 0 22639 0
vsize: 90720
[startup+1080.26 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 22154 0 0 0 107962 74 0 0 25 0 1 0 483825356 92897280 22074 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22680 22074 603 41 0 22639 0
vsize: 90720
[startup+1090.26 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 22154 0 0 0 108962 74 0 0 25 0 1 0 483825356 92897280 22074 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22680 22074 603 41 0 22639 0
vsize: 90720
[startup+1100.26 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 22154 0 0 0 109963 74 0 0 25 0 1 0 483825356 92897280 22074 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22680 22074 603 41 0 22639 0
vsize: 90720
[startup+1110.26 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 22154 0 0 0 110963 74 0 0 25 0 1 0 483825356 92897280 22074 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22680 22074 603 41 0 22639 0
vsize: 90720
[startup+1120.26 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 22154 0 0 0 111963 74 0 0 25 0 1 0 483825356 92897280 22074 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22680 22074 603 41 0 22639 0
vsize: 90720
[startup+1130.26 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 22154 0 0 0 112963 74 0 0 25 0 1 0 483825356 92897280 22074 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22680 22074 603 41 0 22639 0
vsize: 90720
[startup+1140.26 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 22154 0 0 0 113963 74 0 0 25 0 1 0 483825356 92897280 22074 4294967295 134512640 134672761 3221224528 3221223664 134560566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22680 22074 603 41 0 22639 0
vsize: 90720
[startup+1150.26 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 22154 0 0 0 114964 74 0 0 25 0 1 0 483825356 92897280 22074 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22680 22074 603 41 0 22639 0
vsize: 90720
[startup+1160.26 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 22154 0 0 0 115964 74 0 0 25 0 1 0 483825356 92897280 22074 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22680 22074 603 41 0 22639 0
vsize: 90720
[startup+1170.26 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 22154 0 0 0 116964 74 0 0 25 0 1 0 483825356 92897280 22074 4294967295 134512640 134672761 3221224528 3221223664 134560590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22680 22074 603 41 0 22639 0
vsize: 90720
[startup+1180.26 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 22154 0 0 0 117964 74 0 0 25 0 1 0 483825356 92897280 22074 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22680 22074 603 41 0 22639 0
vsize: 90720
[startup+1190.26 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 22154 0 0 0 118964 74 0 0 25 0 1 0 483825356 92897280 22074 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22680 22074 603 41 0 22639 0
vsize: 90720
[startup+1200.26 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29574
Raw data (stat): 29572 (minisat+) R 29571 30701 30700 0 -1 0 22154 0 0 0 119965 74 0 0 25 0 1 0 483825356 92897280 22074 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22680 22074 603 41 0 22639 0
vsize: 90720
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.31 s]
Raw data (loadavg): 0.99 0.97 0.95 1/54 29574
Raw data (stat): 29572 (minisat+) Z 29571 30701 30700 0 -1 12 22157 0 0 0 119965 78 0 0 25 0 1 0 483825356 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.31
CPU time (s): 1200.44
CPU user time (s): 1199.65
CPU system time (s): 0.78388
CPU usage (%): 100.011
Max. virtual memory (Kb): 90720
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####