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/submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-my_adder.opb
MD5SUM	fe8f615a95a6852516985b8e3e78bd85
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	4561
Optimality of the best value was proved	NO
Number of terms in the objective function	577
Biggest coefficient in the objective function	61
Number of bits for the biggest coefficient in the objective function	6
Sum of the numbers in the objective function	24510
Number of bits of the sum of numbers in the objective function	15
Biggest number in a constraint	61
Number of bits of the biggest number in a constraint	6
Biggest sum of numbers in a constraint	24510
Number of bits of the biggest sum of numbers	15
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02584
Number of variables	577
Total number of constraints	1322
Number of constraints which are clauses	1306
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	16
Minimum length of a constraint	2
Maximum length of a constraint	17
Trace number 5969

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc13 THE 2005-04-14 02:32:56 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4391 boxname=wulflinc13 idbench=255 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  fe8f615a95a6852516985b8e3e78bd85  /oldhome/oroussel/tmp/wulflinc13/normalized-my_adder.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc13/normalized-my_adder.opb /oldhome/oroussel/tmp/wulflinc13/normalized-my_adder.opb
IDLAUNCH: 4391
/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:        893852 kB
Buffers:         35324 kB
Cached:          85868 kB
SwapCached:        392 kB
Active:          54660 kB
Inactive:        69796 kB
HighTotal:      131008 kB
HighFree:        41272 kB
LowTotal:       903652 kB
LowFree:        852580 kB
SwapTotal:     2097136 kB
SwapFree:      2096744 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            10856 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 02:52:58 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 4391 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1322 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    1322     4977 |     440       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 6274[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:87831     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         1 |  210130   492551 |   70043       1        7     7.0 |  0.000 % |
c |       101 |  209639   491465 |   77047      98     1983    20.2 |  0.188 % |
c |       251 |  209398   490919 |   84752     246     3047    12.4 |  0.270 % |
c |       477 |  209398   490919 |   93227     472     5320    11.3 |  0.270 % |
c |       814 |  209398   490919 |  102549     809     7426     9.2 |  0.270 % |
c |      1320 |  209398   490919 |  112804    1315    12893     9.8 |  0.270 % |
c |      2079 |  208099   487975 |  124085    2062    18966     9.2 |  0.850 % |
c |      3223 |  207777   487250 |  136493    3203    75259    23.5 |  1.015 % |
c |      4934 |  207777   487250 |  150143    4914   465375    94.7 |  1.015 % |
c |      7496 |  207777   487250 |  165157    7476   523941    70.1 |  1.015 % |
c |     11343 |  207124   485763 |  181673   11316   605974    53.6 |  1.304 % |
c ==============================================================================
c [1mFound solution: 6030[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:63107     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15902 |  341282   799222 |  113760   15812   677541    42.8 |  1.304 % |
c |     16002 |  341282   799222 |  125136   15912   678586    42.6 |  1.292 % |
c |     16153 |  341282   799222 |  137649   16063   680125    42.3 |  1.292 % |
c |     16378 |  341282   799222 |  151414   16288   682659    41.9 |  1.292 % |
c |     16715 |  341282   799222 |  166556   16625   686273    41.3 |  1.292 % |
c |     17222 |  341282   799222 |  183211   17132   689710    40.3 |  1.292 % |
c |     17982 |  341282   799222 |  201532   17892   701677    39.2 |  1.292 % |
c ==============================================================================
c [1mFound solution: 5941[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18575 |  341328   799730 |  113776   18485   726783    39.3 |  1.292 % |
c |     18675 |  341311   799693 |  125153   18584   727472    39.1 |  1.297 % |
c |     18825 |  341311   799693 |  137668   18734   728419    38.9 |  1.297 % |
c |     19050 |  341311   799693 |  151435   18959   730280    38.5 |  1.297 % |
c |     19388 |  341311   799693 |  166579   19297   732516    38.0 |  1.297 % |
c |     19894 |  341311   799693 |  183237   19803   738567    37.3 |  1.297 % |
c |     20653 |  341060   799139 |  201561   20560   748577    36.4 |  1.351 % |
c |     21792 |  341060   799139 |  221717   21699   757149    34.9 |  1.351 % |
c |     23500 |  341060   799139 |  243888   23407   808068    34.5 |  1.351 % |
c |     26064 |  340058   796875 |  268277   25935   888362    34.3 |  1.591 % |
c |     29909 |  340058   796875 |  295105   29780   993861    33.4 |  1.591 % |
c |     35675 |  340058   796875 |  324616   35546  1611580    45.3 |  1.591 % |
c |     44326 |  340058   796875 |  357077   44197  2011857    45.5 |  1.591 % |
c |     57300 |  339999   796741 |  392785   57162  2368847    41.4 |  1.609 % |
c |     76763 |  339999   796741 |  432064   76625  7374052    96.2 |  1.609 % |
c |    105956 |  339999   796741 |  475270  105818  9897084    93.5 |  1.609 % |
c ==============================================================================
c [1mFound solution: 5700[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:64909     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    108372 |  479644  1122919 |  159881  108234 10027671    92.6 |  1.609 % |
c |    108473 |  479644  1122919 |  175869  108335 10028620    92.6 |  1.141 % |
c |    108623 |  479644  1122919 |  193456  108485 10030258    92.5 |  1.141 % |
c |    108848 |  479644  1122919 |  212801  108710 10032710    92.3 |  1.141 % |
c |    109185 |  479644  1122919 |  234081  109047 10045641    92.1 |  1.141 % |
c |    109691 |  479498  1122590 |  257489  109542 10064209    91.9 |  1.162 % |
c |    110451 |  479498  1122590 |  283238  110302 10074504    91.3 |  1.162 % |
c |    111590 |  479498  1122590 |  311562  111441 10093566    90.6 |  1.162 % |
c |    113298 |  479498  1122590 |  342719  113149 10108665    89.3 |  1.162 % |
c |    115860 |  479488  1122570 |  376991  115708 10180504    88.0 |  1.165 % |
c |    119704 |  479488  1122570 |  414690  119552 10487501    87.7 |  1.165 % |
c |    125470 |  479488  1122570 |  456159  125318 11610478    92.6 |  1.165 % |
c |    134119 |  479488  1122570 |  501775  133967 11828437    88.3 |  1.165 % |
c |    147093 |  479488  1122570 |  551952  146941 12479339    84.9 |  1.165 % |
c |    166556 |  479456  1122498 |  607147  166403 15031220    90.3 |  1.175 % |
#### 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.92 0.96 0.91 2/54 5128
Raw data (stat): 5128 (runsolver) R 5127 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422801665 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 7095 0 0 0 982 17 0 0 25 0 1 0 422801665 32923648 6744 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8038 6744 603 41 0 7997 0
vsize: 32152
[startup+20.0015 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 7442 0 0 0 1980 18 0 0 25 0 1 0 422801665 34406400 7091 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8400 7091 603 41 0 8359 0
vsize: 33600
[startup+30.0026 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 7605 0 0 0 2979 19 0 0 25 0 1 0 422801665 35074048 7254 4294967295 134512640 134672761 3221224560 3221223696 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8563 7254 603 41 0 8522 0
vsize: 34252
[startup+40.0028 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 7715 0 0 0 3978 20 0 0 25 0 1 0 422801665 35491840 7364 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8665 7364 603 41 0 8624 0
vsize: 34660
[startup+50.0025 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 7790 0 0 0 4977 21 0 0 25 0 1 0 422801665 35762176 7439 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8731 7439 603 41 0 8690 0
vsize: 34924
[startup+60.0036 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 11934 0 0 0 5969 30 0 0 25 0 1 0 422801665 59572224 11583 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14544 11583 603 41 0 14503 0
vsize: 58176
[startup+70.0038 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 12112 0 0 0 6968 30 0 0 25 0 1 0 422801665 59887616 11761 4294967295 134512640 134672761 3221224560 3221223696 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14621 11761 603 41 0 14580 0
vsize: 58484
[startup+80.0044 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 12212 0 0 0 7967 31 0 0 25 0 1 0 422801665 60293120 11861 4294967295 134512640 134672761 3221224560 3221223712 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14720 11861 603 41 0 14679 0
vsize: 58880
[startup+90.0046 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 12273 0 0 0 8966 32 0 0 25 0 1 0 422801665 60563456 11922 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14786 11922 603 41 0 14745 0
vsize: 59144
[startup+100.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 12309 0 0 0 9966 32 0 0 25 0 1 0 422801665 60690432 11958 4294967295 134512640 134672761 3221224560 3221223728 134560785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14817 11958 603 41 0 14776 0
vsize: 59268
[startup+110.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 12376 0 0 0 10966 32 0 0 25 0 1 0 422801665 60960768 12025 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14883 12025 603 41 0 14842 0
vsize: 59532
[startup+120.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 12445 0 0 0 11965 32 0 0 25 0 1 0 422801665 61222912 12094 4294967295 134512640 134672761 3221224560 3221223696 134560604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14947 12094 603 41 0 14906 0
vsize: 59788
[startup+130.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 12563 0 0 0 12965 33 0 0 25 0 1 0 422801665 61890560 12212 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15110 12212 603 41 0 15069 0
vsize: 60440
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 12748 0 0 0 13964 34 0 0 25 0 1 0 422801665 62566400 12397 4294967295 134512640 134672761 3221224560 3221223648 134555602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15275 12397 603 41 0 15234 0
vsize: 61100
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 13090 0 0 0 14962 35 0 0 25 0 1 0 422801665 64061440 12739 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15640 12739 603 41 0 15599 0
vsize: 62560
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 13139 0 0 0 15962 35 0 0 25 0 1 0 422801665 64192512 12788 4294967295 134512640 134672761 3221224560 3221223720 134561238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15672 12788 603 41 0 15631 0
vsize: 62688
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 13194 0 0 0 16961 36 0 0 25 0 1 0 422801665 64458752 12843 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15737 12843 603 41 0 15696 0
vsize: 62948
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 13258 0 0 0 17961 37 0 0 25 0 1 0 422801665 64729088 12907 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15803 12907 603 41 0 15762 0
vsize: 63212
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 13421 0 0 0 18960 38 0 0 25 0 1 0 422801665 65261568 13070 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15933 13070 603 41 0 15892 0
vsize: 63732
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 13566 0 0 0 19959 38 0 0 25 0 1 0 422801665 65929216 13215 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16096 13215 603 41 0 16055 0
vsize: 64384
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 13641 0 0 0 20959 39 0 0 25 0 1 0 422801665 66195456 13290 4294967295 134512640 134672761 3221224560 3221223760 134557885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16161 13290 603 41 0 16120 0
vsize: 64644
[startup+220.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 13742 0 0 0 21958 39 0 0 25 0 1 0 422801665 66605056 13391 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16261 13391 603 41 0 16220 0
vsize: 65044
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 13801 0 0 0 22958 40 0 0 25 0 1 0 422801665 66871296 13450 4294967295 134512640 134672761 3221224560 3221223728 134561261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16326 13450 603 41 0 16285 0
vsize: 65304
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 13873 0 0 0 23957 41 0 0 25 0 1 0 422801665 67133440 13522 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16390 13522 603 41 0 16349 0
vsize: 65560
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 13948 0 0 0 24956 41 0 0 25 0 1 0 422801665 67395584 13597 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16454 13597 603 41 0 16413 0
vsize: 65816
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 14024 0 0 0 25955 42 0 0 25 0 1 0 422801665 67796992 13673 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16552 13673 603 41 0 16511 0
vsize: 66208
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 14089 0 0 0 26954 43 0 0 25 0 1 0 422801665 68059136 13738 4294967295 134512640 134672761 3221224560 3221223728 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16616 13738 603 41 0 16575 0
vsize: 66464
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 14217 0 0 0 27954 43 0 0 25 0 1 0 422801665 68464640 13866 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16715 13866 603 41 0 16674 0
vsize: 66860
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 14451 0 0 0 28953 44 0 0 25 0 1 0 422801665 69533696 14100 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16976 14100 603 41 0 16935 0
vsize: 67904
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 14637 0 0 0 29952 45 0 0 25 0 1 0 422801665 70205440 14286 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17140 14286 603 41 0 17099 0
vsize: 68560
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 14900 0 0 0 30952 46 0 0 25 0 1 0 422801665 71282688 14549 4294967295 134512640 134672761 3221224560 3221223632 134553544 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17403 14549 603 41 0 17362 0
vsize: 69612
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 15092 0 0 0 31951 47 0 0 25 0 1 0 422801665 72089600 14741 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17600 14741 603 41 0 17559 0
vsize: 70400
[startup+330.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 15348 0 0 0 32951 47 0 0 25 0 1 0 422801665 73134080 14997 4294967295 134512640 134672761 3221224560 3221223728 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17855 14997 603 41 0 17814 0
vsize: 71420
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 15604 0 0 0 33950 48 0 0 25 0 1 0 422801665 74219520 15253 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18120 15253 603 41 0 18079 0
vsize: 72480
[startup+350.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 15855 0 0 0 34950 49 0 0 25 0 1 0 422801665 75165696 15504 4294967295 134512640 134672761 3221224560 3221223728 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18351 15504 603 41 0 18310 0
vsize: 73404
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 16101 0 0 0 35949 49 0 0 25 0 1 0 422801665 76218368 15750 4294967295 134512640 134672761 3221224560 3221223664 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18608 15750 603 41 0 18567 0
vsize: 74432
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 16318 0 0 0 36949 50 0 0 25 0 1 0 422801665 77144064 15967 4294967295 134512640 134672761 3221224560 3221223760 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18834 15967 603 41 0 18793 0
vsize: 75336
[startup+380.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 16536 0 0 0 37949 51 0 0 25 0 1 0 422801665 78200832 16185 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19092 16185 603 41 0 19051 0
vsize: 76368
[startup+390.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 16776 0 0 0 38948 51 0 0 25 0 1 0 422801665 79273984 16425 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19354 16425 603 41 0 19313 0
vsize: 77416
[startup+400.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 16978 0 0 0 39947 52 0 0 25 0 1 0 422801665 80084992 16627 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19552 16627 603 41 0 19511 0
vsize: 78208
[startup+410.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 17210 0 0 0 40947 53 0 0 25 0 1 0 422801665 81027072 16859 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19782 16859 603 41 0 19741 0
vsize: 79128
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 17463 0 0 0 41946 53 0 0 25 0 1 0 422801665 82108416 17112 4294967295 134512640 134672761 3221224560 3221223744 134558638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20046 17112 603 41 0 20005 0
vsize: 80184
[startup+430.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 17712 0 0 0 42946 54 0 0 25 0 1 0 422801665 83030016 17361 4294967295 134512640 134672761 3221224560 3221223696 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20271 17361 603 41 0 20230 0
vsize: 81084
[startup+440.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 17907 0 0 0 43946 54 0 0 25 0 1 0 422801665 83836928 17556 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20468 17556 603 41 0 20427 0
vsize: 81872
[startup+450.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 18139 0 0 0 44946 55 0 0 25 0 1 0 422801665 84750336 17788 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20691 17788 603 41 0 20650 0
vsize: 82764
[startup+460.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 18299 0 0 0 45946 55 0 0 25 0 1 0 422801665 85422080 17948 4294967295 134512640 134672761 3221224560 3221223664 134559998 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20855 17948 603 41 0 20814 0
vsize: 83420
[startup+470.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 18578 0 0 0 46945 55 0 0 25 0 1 0 422801665 86626304 18227 4294967295 134512640 134672761 3221224560 3221223664 134559875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21149 18227 603 41 0 21108 0
vsize: 84596
[startup+480.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 18826 0 0 0 47945 56 0 0 25 0 1 0 422801665 87560192 18475 4294967295 134512640 134672761 3221224560 3221223744 134558775 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21377 18475 603 41 0 21336 0
vsize: 85508
[startup+490.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 19038 0 0 0 48945 57 0 0 25 0 1 0 422801665 88477696 18687 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21601 18687 603 41 0 21560 0
vsize: 86404
[startup+500.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 19106 0 0 0 49945 57 0 0 25 0 1 0 422801665 88743936 18755 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21666 18756 603 41 0 21625 0
vsize: 86664
[startup+510.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 19176 0 0 0 50945 57 0 0 25 0 1 0 422801665 89014272 18825 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21732 18825 603 41 0 21691 0
vsize: 86928
[startup+520.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 19374 0 0 0 51943 58 0 0 25 0 1 0 422801665 89829376 19023 4294967295 134512640 134672761 3221224560 3221223664 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21931 19023 603 41 0 21890 0
vsize: 87724
[startup+530.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 19636 0 0 0 52943 59 0 0 25 0 1 0 422801665 90914816 19285 4294967295 134512640 134672761 3221224560 3221223696 134560645 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22196 19285 603 41 0 22155 0
vsize: 88784
[startup+540.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 19815 0 0 0 53942 59 0 0 25 0 1 0 422801665 91590656 19464 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22361 19464 603 41 0 22320 0
vsize: 89444
[startup+550.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 20167 0 0 0 54941 61 0 0 25 0 1 0 422801665 93069312 19816 4294967295 134512640 134672761 3221224560 3221223664 134560279 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22722 19816 603 41 0 22681 0
vsize: 90888
[startup+560.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 20357 0 0 0 55941 61 0 0 25 0 1 0 422801665 93876224 20006 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22919 20006 603 41 0 22878 0
vsize: 91676
[startup+570.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 20605 0 0 0 56940 62 0 0 25 0 1 0 422801665 94810112 20254 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23147 20254 603 41 0 23106 0
vsize: 92588
[startup+580.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 20713 0 0 0 57940 62 0 0 25 0 1 0 422801665 95215616 20362 4294967295 134512640 134672761 3221224560 3221223728 134561269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23246 20362 603 41 0 23205 0
vsize: 92984
[startup+590.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 20951 0 0 0 58939 63 0 0 25 0 1 0 422801665 96292864 20600 4294967295 134512640 134672761 3221224560 3221223728 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23509 20600 603 41 0 23468 0
vsize: 94036
[startup+600.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 21129 0 0 0 59939 64 0 0 25 0 1 0 422801665 96964608 20778 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23673 20778 603 41 0 23632 0
vsize: 94692
[startup+610.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 21298 0 0 0 60939 64 0 0 25 0 1 0 422801665 97644544 20947 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23839 20947 603 41 0 23798 0
vsize: 95356
[startup+620.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 21416 0 0 0 61938 65 0 0 25 0 1 0 422801665 98177024 21065 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23969 21065 603 41 0 23928 0
vsize: 95876
[startup+630.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 21615 0 0 0 62938 65 0 0 25 0 1 0 422801665 98983936 21264 4294967295 134512640 134672761 3221224560 3221223664 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24166 21264 603 41 0 24125 0
vsize: 96664
[startup+640.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 21824 0 0 0 63937 66 0 0 25 0 1 0 422801665 99782656 21473 4294967295 134512640 134672761 3221224560 3221223728 134561025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24361 21473 603 41 0 24320 0
vsize: 97444
[startup+650.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 22024 0 0 0 64936 67 0 0 25 0 1 0 422801665 100589568 21673 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24558 21673 603 41 0 24517 0
vsize: 98232
[startup+660.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 26839 0 0 0 65927 77 0 0 25 0 1 0 422801665 116035584 26158 4294967295 134512640 134672761 3221224560 3221223716 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28329 26158 603 41 0 28288 0
vsize: 113316
[startup+670.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 26900 0 0 0 66927 77 0 0 25 0 1 0 422801665 116170752 26219 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28362 26219 603 41 0 28321 0
vsize: 113448
[startup+680.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 26995 0 0 0 67926 78 0 0 25 0 1 0 422801665 116572160 26314 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28460 26314 603 41 0 28419 0
vsize: 113840
[startup+690.019 s]
Raw data (loadavg): 1.07 0.99 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 27040 0 0 0 68926 78 0 0 25 0 1 0 422801665 116842496 26359 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28526 26359 603 41 0 28485 0
vsize: 114104
[startup+700.018 s]
Raw data (loadavg): 1.14 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 27084 0 0 0 69926 78 0 0 25 0 1 0 422801665 116977664 26403 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28559 26403 603 41 0 28518 0
vsize: 114236
[startup+710.019 s]
Raw data (loadavg): 1.11 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 27170 0 0 0 70926 78 0 0 25 0 1 0 422801665 117248000 26489 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28625 26489 603 41 0 28584 0
vsize: 114500
[startup+720.019 s]
Raw data (loadavg): 1.10 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 27267 0 0 0 71926 78 0 0 25 0 1 0 422801665 117653504 26586 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28724 26586 603 41 0 28683 0
vsize: 114896
[startup+730.019 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 27384 0 0 0 72926 79 0 0 25 0 1 0 422801665 118185984 26703 4294967295 134512640 134672761 3221224560 3221223704 134560630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28854 26703 603 41 0 28813 0
vsize: 115416
[startup+740.02 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 27518 0 0 0 73925 80 0 0 25 0 1 0 422801665 118722560 26837 4294967295 134512640 134672761 3221224560 3221223664 134559890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28985 26837 603 41 0 28944 0
vsize: 115940
[startup+750.02 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 27601 0 0 0 74925 80 0 0 25 0 1 0 422801665 118992896 26920 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29051 26920 603 41 0 29010 0
vsize: 116204
[startup+760.02 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 27930 0 0 0 75924 81 0 0 25 0 1 0 422801665 120352768 27249 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29383 27249 603 41 0 29342 0
vsize: 117532
[startup+770.02 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 28117 0 0 0 76924 82 0 0 25 0 1 0 422801665 121163776 27436 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29581 27436 603 41 0 29540 0
vsize: 118324
[startup+780.021 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 28387 0 0 0 77923 83 0 0 25 0 1 0 422801665 122241024 27706 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29844 27706 603 41 0 29803 0
vsize: 119376
[startup+790.02 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 28580 0 0 0 78923 83 0 0 25 0 1 0 422801665 123052032 27899 4294967295 134512640 134672761 3221224560 3221223712 134565056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30042 27899 603 41 0 30001 0
vsize: 120168
[startup+800.02 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 28633 0 0 0 79923 83 0 0 25 0 1 0 422801665 123183104 27952 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 27952 603 41 0 30033 0
vsize: 120296
[startup+810.021 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 28688 0 0 0 80922 84 0 0 25 0 1 0 422801665 123449344 28007 4294967295 134512640 134672761 3221224560 3221223728 134561127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30139 28007 603 41 0 30098 0
vsize: 120556
[startup+820.02 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 28753 0 0 0 81922 84 0 0 25 0 1 0 422801665 123715584 28072 4294967295 134512640 134672761 3221224560 3221223664 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30204 28072 603 41 0 30163 0
vsize: 120816
[startup+830.021 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 28816 0 0 0 82922 84 0 0 25 0 1 0 422801665 124502016 28135 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30396 28135 603 41 0 30355 0
vsize: 121584
[startup+840.021 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 28902 0 0 0 83922 85 0 0 25 0 1 0 422801665 124899328 28221 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30493 28221 603 41 0 30452 0
vsize: 121972
[startup+850.021 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 29072 0 0 0 84922 85 0 0 25 0 1 0 422801665 125571072 28391 4294967295 134512640 134672761 3221224560 3221223696 134560598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30657 28391 603 41 0 30616 0
vsize: 122628
[startup+860.021 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 29145 0 0 0 85922 85 0 0 25 0 1 0 422801665 125841408 28464 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30723 28464 603 41 0 30682 0
vsize: 122892
[startup+870.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 29230 0 0 0 86921 86 0 0 25 0 1 0 422801665 126242816 28549 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30821 28549 603 41 0 30780 0
vsize: 123284
[startup+880.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 29318 0 0 0 87921 86 0 0 25 0 1 0 422801665 126509056 28637 4294967295 134512640 134672761 3221224560 3221223696 134560566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30886 28637 603 41 0 30845 0
vsize: 123544
[startup+890.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 29381 0 0 0 88921 86 0 0 25 0 1 0 422801665 126779392 28700 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30952 28700 603 41 0 30911 0
vsize: 123808
[startup+900.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 29462 0 0 0 89921 87 0 0 25 0 1 0 422801665 127045632 28781 4294967295 134512640 134672761 3221224560 3221223728 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31017 28781 603 41 0 30976 0
vsize: 124068
[startup+910.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 29550 0 0 0 90921 87 0 0 25 0 1 0 422801665 127447040 28869 4294967295 134512640 134672761 3221224560 3221223696 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31115 28869 603 41 0 31074 0
vsize: 124460
[startup+920.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 29634 0 0 0 91921 87 0 0 25 0 1 0 422801665 127844352 28953 4294967295 134512640 134672761 3221224560 3221223728 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31212 28953 603 41 0 31171 0
vsize: 124848
[startup+930.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 29723 0 0 0 92921 88 0 0 25 0 1 0 422801665 128114688 29042 4294967295 134512640 134672761 3221224560 3221223696 134560585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31278 29042 603 41 0 31237 0
vsize: 125112
[startup+940.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 29784 0 0 0 93921 88 0 0 25 0 1 0 422801665 128385024 29103 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31344 29103 603 41 0 31303 0
vsize: 125376
[startup+950.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 29932 0 0 0 94920 88 0 0 25 0 1 0 422801665 129060864 29251 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31509 29251 603 41 0 31468 0
vsize: 126036
[startup+960.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 30088 0 0 0 95920 89 0 0 25 0 1 0 422801665 129597440 29407 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31640 29407 603 41 0 31599 0
vsize: 126560
[startup+970.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 30184 0 0 0 96920 89 0 0 25 0 1 0 422801665 130002944 29503 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31739 29503 603 41 0 31698 0
vsize: 126956
[startup+980.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 30316 0 0 0 97920 90 0 0 25 0 1 0 422801665 130539520 29635 4294967295 134512640 134672761 3221224560 3221223760 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31870 29635 603 41 0 31829 0
vsize: 127480
[startup+990.023 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 30466 0 0 0 98920 90 0 0 25 0 1 0 422801665 131211264 29785 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32034 29785 603 41 0 31993 0
vsize: 128136
[startup+1000.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 30639 0 0 0 99919 91 0 0 25 0 1 0 422801665 131891200 29958 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32200 29958 603 41 0 32159 0
vsize: 128800
[startup+1010.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 30831 0 0 0 100918 92 0 0 25 0 1 0 422801665 132706304 30150 4294967295 134512640 134672761 3221224560 3221223760 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32399 30150 603 41 0 32358 0
vsize: 129596
[startup+1020.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 31018 0 0 0 101918 92 0 0 25 0 1 0 422801665 133513216 30337 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32596 30337 603 41 0 32555 0
vsize: 130384
[startup+1030.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 31222 0 0 0 102918 92 0 0 25 0 1 0 422801665 134291456 30541 4294967295 134512640 134672761 3221224560 3221223664 134560154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32786 30541 603 41 0 32745 0
vsize: 131144
[startup+1040.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 31410 0 0 0 103918 93 0 0 25 0 1 0 422801665 135090176 30729 4294967295 134512640 134672761 3221224560 3221223664 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32981 30729 603 41 0 32940 0
vsize: 131924
[startup+1050.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 31583 0 0 0 104917 93 0 0 25 0 1 0 422801665 135766016 30902 4294967295 134512640 134672761 3221224560 3221223696 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33146 30902 603 41 0 33105 0
vsize: 132584
[startup+1060.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 31691 0 0 0 105917 94 0 0 25 0 1 0 422801665 136171520 31010 4294967295 134512640 134672761 3221224560 3221223708 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33245 31010 603 41 0 33204 0
vsize: 132980
[startup+1070.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 31783 0 0 0 106917 94 0 0 25 0 1 0 422801665 136572928 31102 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33343 31102 603 41 0 33302 0
vsize: 133372
[startup+1080.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 31925 0 0 0 107917 95 0 0 25 0 1 0 422801665 137113600 31244 4294967295 134512640 134672761 3221224560 3221223664 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33475 31244 603 41 0 33434 0
vsize: 133900
[startup+1090.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 32083 0 0 0 108916 96 0 0 25 0 1 0 422801665 137789440 31402 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33640 31402 603 41 0 33599 0
vsize: 134560
[startup+1100.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 32140 0 0 0 109916 96 0 0 25 0 1 0 422801665 138059776 31459 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33706 31459 603 41 0 33665 0
vsize: 134824
[startup+1110.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 32194 0 0 0 110916 96 0 0 25 0 1 0 422801665 138194944 31513 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33739 31513 603 41 0 33698 0
vsize: 134956
[startup+1120.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 32237 0 0 0 111916 96 0 0 25 0 1 0 422801665 138326016 31556 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33771 31556 603 41 0 33730 0
vsize: 135084
[startup+1130.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 32264 0 0 0 112916 97 0 0 25 0 1 0 422801665 138461184 31583 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33804 31583 603 41 0 33763 0
vsize: 135216
[startup+1140.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 32296 0 0 0 113916 97 0 0 25 0 1 0 422801665 138596352 31615 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33837 31615 603 41 0 33796 0
vsize: 135348
[startup+1150.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 32402 0 0 0 114915 97 0 0 25 0 1 0 422801665 139001856 31721 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33936 31721 603 41 0 33895 0
vsize: 135744
[startup+1160.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 32450 0 0 0 115915 98 0 0 25 0 1 0 422801665 139268096 31769 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34001 31769 603 41 0 33960 0
vsize: 136004
[startup+1170.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 32528 0 0 0 116915 98 0 0 25 0 1 0 422801665 139538432 31847 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34067 31847 603 41 0 34026 0
vsize: 136268
[startup+1180.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 32627 0 0 0 117915 98 0 0 25 0 1 0 422801665 139935744 31946 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34164 31946 603 41 0 34123 0
vsize: 136656
[startup+1190.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 32830 0 0 0 118915 98 0 0 25 0 1 0 422801665 140738560 32149 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34360 32149 603 41 0 34319 0
vsize: 137440
[startup+1200.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5128
Raw data (stat): 5128 (minisat+) R 5127 30701 30700 0 -1 0 32989 0 0 0 119914 99 0 0 25 0 1 0 422801665 141410304 32308 4294967295 134512640 134672761 3221224560 3221223728 134561261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34524 32308 603 41 0 34483 0
vsize: 138096
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 1.00 1.00 0.92 1/54 5128
Raw data (stat): 5128 (minisat+) Z 5127 30701 30700 0 -1 12 32992 0 0 0 119914 105 0 0 25 0 1 0 422801665 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.09
CPU time (s): 1200.2
CPU user time (s): 1199.15
CPU system time (s): 1.05484
CPU usage (%): 100.01
Max. virtual memory (Kb): 138096
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####