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-mux.opb
MD5SUM	fa7153262db792d01bec14f5a651af5b
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	872
Optimality of the best value was proved	NO
Number of terms in the objective function	232
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	9597
Number of bits of the sum of numbers in the objective function	14
Biggest number in a constraint	61
Number of bits of the biggest number in a constraint	6
Biggest sum of numbers in a constraint	9597
Number of bits of the biggest sum of numbers	14
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	0.332949
Number of variables	232
Total number of constraints	527
Number of constraints which are clauses	527
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	27
Trace number 6344

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc27 THE 2005-04-14 04:22:51 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4766 boxname=wulflinc27 idbench=254 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  fa7153262db792d01bec14f5a651af5b  /oldhome/oroussel/tmp/wulflinc27/normalized-mux.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc27/normalized-mux.opb /oldhome/oroussel/tmp/wulflinc27/normalized-mux.opb
IDLAUNCH: 4766
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
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	: 3
cpu MHz		: 451.169
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	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        841268 kB
Buffers:         35220 kB
Cached:         121284 kB
SwapCached:       3160 kB
Active:          69836 kB
Inactive:        92684 kB
HighTotal:      131008 kB
HighFree:         6328 kB
LowTotal:       903652 kB
LowFree:        834940 kB
SwapTotal:     2097892 kB
SwapFree:      2094732 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            25376 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 04:42:54 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 4766 7 1200.21 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 527 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 |     527     2331 |     175       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 1330[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:29793     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   79991   188331 |   26663       0        0     nan |  0.000 % |
c |       100 |   79991   188331 |   29329     100      632     6.3 |  0.004 % |
c |       251 |   79991   188331 |   32262     251    11278    44.9 |  0.004 % |
c |       476 |   79380   186945 |   35488     468    15089    32.2 |  0.579 % |
c |       813 |   79380   186945 |   39037     805    32211    40.0 |  0.579 % |
c |      1319 |   79380   186945 |   42941    1311    58690    44.8 |  0.579 % |
c |      2078 |   79380   186945 |   47235    2070   159961    77.3 |  0.579 % |
c |      3217 |   79380   186945 |   51958    3209   283438    88.3 |  0.579 % |
c |      4925 |   79380   186945 |   57154    4917   378144    76.9 |  0.579 % |
c |      7487 |   79380   186945 |   62869    7479   663336    88.7 |  0.579 % |
c |     11331 |   79334   186840 |   69156   11321  1075725    95.0 |  0.632 % |
c ==============================================================================
c [1mFound solution: 1314[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:24283     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11709 |  144057   338412 |   48019   11699  1106195    94.6 |  0.632 % |
c |     11809 |  144057   338412 |   52820   11799  1108302    93.9 |  0.352 % |
c |     11960 |  144022   338332 |   58102   11948  1109245    92.8 |  0.373 % |
c |     12187 |  143914   338090 |   63913   12174  1113381    91.5 |  0.429 % |
c |     12525 |  143914   338090 |   70304   12512  1133314    90.6 |  0.430 % |
c |     13032 |  143914   338090 |   77335   13019  1152376    88.5 |  0.429 % |
c |     13791 |  143914   338090 |   85068   13778  1184576    86.0 |  0.429 % |
c |     14932 |  143856   337961 |   93575   14917  1210294    81.1 |  0.461 % |
c |     16643 |  143838   337922 |  102932   16624  1262552    75.9 |  0.471 % |
c ==============================================================================
c [1mFound solution: 1272[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17405 |  144582   339872 |   48194   17385  1274377    73.3 |  0.471 % |
c |     17506 |  144183   338971 |   53013   17440  1275574    73.1 |  0.712 % |
c |     17662 |  144183   338971 |   58314   17596  1285159    73.0 |  0.712 % |
c |     17887 |  144183   338971 |   64146   17821  1298314    72.9 |  0.712 % |
c ==============================================================================
c [1mFound solution: 1262[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18037 |  144254   339176 |   48084   17971  1304032    72.6 |  0.712 % |
c |     18139 |  144254   339176 |   52892   18073  1304877    72.2 |  0.714 % |
c |     18290 |  144254   339176 |   58181   18224  1315158    72.2 |  0.714 % |
c |     18516 |  144176   339001 |   63999   18447  1318937    71.5 |  0.756 % |
c ==============================================================================
c [1mFound solution: 1261[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18577 |  144571   340012 |   48190   18508  1319859    71.3 |  0.756 % |
c |     18677 |  144571   340012 |   53009   18608  1321739    71.0 |  0.757 % |
c ==============================================================================
c [1mFound solution: 1252[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 |     18694 |  144579   340032 |   48193   18625  1324809    71.1 |  0.757 % |
c |     18794 |  144579   340032 |   53012   18725  1325888    70.8 |  0.759 % |
c ==============================================================================
c [1mFound solution: 1235[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18800 |  145198   341578 |   48399   18731  1326305    70.8 |  0.759 % |
c |     18900 |  145198   341578 |   53238   18831  1336263    71.0 |  0.766 % |
c |     19050 |  145198   341578 |   58562   18981  1345959    70.9 |  0.766 % |
c |     19276 |  145198   341578 |   64419   19207  1358938    70.8 |  0.766 % |
c |     19614 |  145198   341578 |   70860   19545  1363796    69.8 |  0.766 % |
c |     20120 |  145198   341578 |   77947   20051  1370317    68.3 |  0.767 % |
c ==============================================================================
c [1mFound solution: 1224[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20357 |  145218   341628 |   48406   20288  1385001    68.3 |  0.767 % |
c ==============================================================================
c [1mFound solution: 1191[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20396 |  145235   341671 |   48411   20327  1389100    68.3 |  0.767 % |
c |     20496 |  145235   341671 |   53252   20427  1391555    68.1 |  0.770 % |
c |     20647 |  145235   341671 |   58577   20578  1395264    67.8 |  0.770 % |
c |     20872 |  145235   341671 |   64435   20803  1402407    67.4 |  0.770 % |
c ==============================================================================
c [1mFound solution: 1186[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21035 |  145248   341702 |   48416   20966  1408753    67.2 |  0.770 % |
c ==============================================================================
c [1mFound solution: 1183[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21053 |  145264   341740 |   48421   20984  1409028    67.1 |  0.770 % |
c ==============================================================================
c [1mFound solution: 1150[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21089 |  145305   341844 |   48435   21020  1413109    67.2 |  0.770 % |
c |     21189 |  145305   341844 |   53278   21120  1416180    67.1 |  0.776 % |
c |     21341 |  145305   341844 |   58606   21272  1419123    66.7 |  0.776 % |
c |     21567 |  145305   341844 |   64466   21498  1436119    66.8 |  0.776 % |
c |     21907 |  145305   341844 |   70913   21838  1443566    66.1 |  0.776 % |
c |     22414 |  145305   341844 |   78005   22345  1458946    65.3 |  0.776 % |
c |     23173 |  145279   341786 |   85805   23102  1472087    63.7 |  0.791 % |
c |     24312 |  145279   341786 |   94386   24241  1489082    61.4 |  0.791 % |
c |     26022 |  145275   341777 |  103824   25950  1532795    59.1 |  0.793 % |
c |     28586 |  145275   341777 |  114207   28514  1691048    59.3 |  0.793 % |
c |     32430 |  145275   341777 |  125627   32358  1957101    60.5 |  0.793 % |
c |     38198 |  145275   341777 |  138190   38126  2316948    60.8 |  0.793 % |
c |     46848 |  145275   341777 |  152009   46776  2786145    59.6 |  0.793 % |
c |     59822 |  145275   341777 |  167210   59750  3571379    59.8 |  0.793 % |
c |     79284 |  145275   341777 |  183931   79212  5034921    63.6 |  0.793 % |
c |    108479 |  145275   341777 |  202325  108407  6526044    60.2 |  0.793 % |
#### 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.84 0.94 0.90 2/54 25120
Raw data (stat): 25120 (runsolver) R 25119 18865 18864 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481676655 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 2729 0 0 0 992 6 0 0 25 0 1 0 481676655 13070336 2654 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3191 2654 603 41 0 3150 0
vsize: 12764
[startup+19.9998 s]
Raw data (loadavg): 0.89 0.94 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 2930 0 0 0 1990 7 0 0 25 0 1 0 481676655 13881344 2855 4294967295 134512640 134672761 3221224576 3221223776 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3389 2855 603 41 0 3348 0
vsize: 13556
[startup+30.0009 s]
Raw data (loadavg): 0.90 0.94 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 3205 0 0 0 2990 8 0 0 25 0 1 0 481676655 14934016 3130 4294967295 134512640 134672761 3221224576 3221223760 134559383 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3646 3130 603 41 0 3605 0
vsize: 14584
[startup+40.0008 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 3388 0 0 0 3989 9 0 0 25 0 1 0 481676655 15728640 3313 4294967295 134512640 134672761 3221224576 3221223712 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3840 3313 603 41 0 3799 0
vsize: 15360
[startup+50.0013 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 3607 0 0 0 4988 9 0 0 25 0 1 0 481676655 16654336 3532 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4066 3532 603 41 0 4025 0
vsize: 16264
[startup+60.0014 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 5571 0 0 0 5984 14 0 0 25 0 1 0 481676655 25649152 5408 4294967295 134512640 134672761 3221224576 3221223712 134560634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6262 5408 603 41 0 6221 0
vsize: 25048
[startup+70.0012 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 5662 0 0 0 6984 14 0 0 25 0 1 0 481676655 25919488 5499 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6328 5499 603 41 0 6287 0
vsize: 25312
[startup+80.0017 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 5739 0 0 0 7984 14 0 0 25 0 1 0 481676655 26370048 5576 4294967295 134512640 134672761 3221224576 3221223744 134560845 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6438 5576 603 41 0 6397 0
vsize: 25752
[startup+90.0019 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 5900 0 0 0 8983 15 0 0 25 0 1 0 481676655 26828800 5724 4294967295 134512640 134672761 3221224576 3221223680 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6550 5724 603 41 0 6509 0
vsize: 26200
[startup+100.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 6024 0 0 0 9983 15 0 0 25 0 1 0 481676655 27045888 5776 4294967295 134512640 134672761 3221224576 3221223720 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6603 5776 603 41 0 6562 0
vsize: 26412
[startup+110.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 6140 0 0 0 10983 16 0 0 25 0 1 0 481676655 27246592 5838 4294967295 134512640 134672761 3221224576 3221223712 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6652 5838 603 41 0 6611 0
vsize: 26608
[startup+120.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 6277 0 0 0 11982 16 0 0 25 0 1 0 481676655 27643904 5906 4294967295 134512640 134672761 3221224576 3221223748 134556646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6749 5906 603 41 0 6708 0
vsize: 26996
[startup+130.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 6367 0 0 0 12982 17 0 0 25 0 1 0 481676655 27914240 5996 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6815 5996 603 41 0 6774 0
vsize: 27260
[startup+140.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 6424 0 0 0 13982 17 0 0 25 0 1 0 481676655 28176384 6053 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6879 6053 603 41 0 6838 0
vsize: 27516
[startup+150.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 6544 0 0 0 14982 17 0 0 25 0 1 0 481676655 28721152 6173 4294967295 134512640 134672761 3221224576 3221223776 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7012 6173 603 41 0 6971 0
vsize: 28048
[startup+160.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 6608 0 0 0 15982 17 0 0 25 0 1 0 481676655 28848128 6237 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7043 6237 603 41 0 7002 0
vsize: 28172
[startup+170.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 6690 0 0 0 16982 17 0 0 25 0 1 0 481676655 29241344 6319 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7139 6319 603 41 0 7098 0
vsize: 28556
[startup+180.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 6801 0 0 0 17982 18 0 0 25 0 1 0 481676655 29642752 6430 4294967295 134512640 134672761 3221224576 3221223744 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7237 6430 603 41 0 7196 0
vsize: 28948
[startup+190.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 6905 0 0 0 18982 18 0 0 25 0 1 0 481676655 30306304 6534 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7399 6534 603 41 0 7358 0
vsize: 29596
[startup+200.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 6988 0 0 0 19982 18 0 0 25 0 1 0 481676655 30572544 6617 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7464 6617 603 41 0 7423 0
vsize: 29856
[startup+210.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 7069 0 0 0 20982 18 0 0 25 0 1 0 481676655 30973952 6698 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7562 6698 603 41 0 7521 0
vsize: 30248
[startup+220.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 7144 0 0 0 21982 19 0 0 25 0 1 0 481676655 31244288 6773 4294967295 134512640 134672761 3221224576 3221223740 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7628 6773 603 41 0 7587 0
vsize: 30512
[startup+230.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 7216 0 0 0 22982 19 0 0 25 0 1 0 481676655 31506432 6845 4294967295 134512640 134672761 3221224576 3221223728 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7692 6845 603 41 0 7651 0
vsize: 30768
[startup+240.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 7285 0 0 0 23981 19 0 0 25 0 1 0 481676655 31768576 6914 4294967295 134512640 134672761 3221224576 3221223680 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7756 6914 603 41 0 7715 0
vsize: 31024
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 7369 0 0 0 24981 20 0 0 25 0 1 0 481676655 32161792 6998 4294967295 134512640 134672761 3221224576 3221223744 134560797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7852 6998 603 41 0 7811 0
vsize: 31408
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 7448 0 0 0 25981 20 0 0 25 0 1 0 481676655 32432128 7077 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7918 7077 603 41 0 7877 0
vsize: 31672
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 7514 0 0 0 26981 20 0 0 25 0 1 0 481676655 32694272 7143 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7982 7143 603 41 0 7941 0
vsize: 31928
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 7580 0 0 0 27981 20 0 0 25 0 1 0 481676655 32956416 7209 4294967295 134512640 134672761 3221224576 3221223740 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8046 7209 603 41 0 8005 0
vsize: 32184
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 7642 0 0 0 28982 20 0 0 25 0 1 0 481676655 33218560 7271 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8110 7271 603 41 0 8069 0
vsize: 32440
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 7710 0 0 0 29981 21 0 0 25 0 1 0 481676655 33480704 7339 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8174 7339 603 41 0 8133 0
vsize: 32696
[startup+310.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 7770 0 0 0 30981 21 0 0 25 0 1 0 481676655 33746944 7399 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8239 7399 603 41 0 8198 0
vsize: 32956
[startup+320.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 7835 0 0 0 31981 21 0 0 25 0 1 0 481676655 34009088 7464 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8303 7464 603 41 0 8262 0
vsize: 33212
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 7908 0 0 0 32981 21 0 0 25 0 1 0 481676655 34283520 7537 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8370 7537 603 41 0 8329 0
vsize: 33480
[startup+340.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 7961 0 0 0 33981 21 0 0 25 0 1 0 481676655 34545664 7590 4294967295 134512640 134672761 3221224576 3221223744 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8434 7590 603 41 0 8393 0
vsize: 33736
[startup+350.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 8029 0 0 0 34981 21 0 0 25 0 1 0 481676655 34816000 7658 4294967295 134512640 134672761 3221224576 3221223744 134560797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8500 7658 603 41 0 8459 0
vsize: 34000
[startup+360.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 8096 0 0 0 35982 22 0 0 25 0 1 0 481676655 35082240 7725 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8565 7725 603 41 0 8524 0
vsize: 34260
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 8165 0 0 0 36981 22 0 0 25 0 1 0 481676655 35344384 7794 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8629 7794 603 41 0 8588 0
vsize: 34516
[startup+380.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 8239 0 0 0 37982 22 0 0 25 0 1 0 481676655 35622912 7868 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8697 7868 603 41 0 8656 0
vsize: 34788
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 8313 0 0 0 38981 22 0 0 25 0 1 0 481676655 36024320 7942 4294967295 134512640 134672761 3221224576 3221223760 134559532 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8795 7942 603 41 0 8754 0
vsize: 35180
[startup+400.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 8379 0 0 0 39982 23 0 0 25 0 1 0 481676655 36294656 8008 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8861 8008 603 41 0 8820 0
vsize: 35444
[startup+410.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 8442 0 0 0 40982 23 0 0 25 0 1 0 481676655 36560896 8071 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8926 8071 603 41 0 8885 0
vsize: 35704
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 8512 0 0 0 41981 23 0 0 25 0 1 0 481676655 36823040 8141 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8990 8141 603 41 0 8949 0
vsize: 35960
[startup+430.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 8586 0 0 0 42981 23 0 0 25 0 1 0 481676655 37089280 8215 4294967295 134512640 134672761 3221224576 3221223760 134558382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9055 8215 603 41 0 9014 0
vsize: 36220
[startup+440.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 8655 0 0 0 43981 24 0 0 25 0 1 0 481676655 37351424 8284 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9119 8284 603 41 0 9078 0
vsize: 36476
[startup+450.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 8728 0 0 0 44981 24 0 0 25 0 1 0 481676655 37752832 8357 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9217 8357 603 41 0 9176 0
vsize: 36868
[startup+460.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 8792 0 0 0 45981 24 0 0 25 0 1 0 481676655 37888000 8421 4294967295 134512640 134672761 3221224576 3221223744 134560828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9250 8421 603 41 0 9209 0
vsize: 37000
[startup+470.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 8854 0 0 0 46980 25 0 0 25 0 1 0 481676655 38150144 8483 4294967295 134512640 134672761 3221224576 3221223680 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9314 8483 603 41 0 9273 0
vsize: 37256
[startup+480.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 8910 0 0 0 47980 25 0 0 25 0 1 0 481676655 38420480 8539 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9380 8539 603 41 0 9339 0
vsize: 37520
[startup+490.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 9004 0 0 0 48980 25 0 0 25 0 1 0 481676655 38813696 8633 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9476 8633 603 41 0 9435 0
vsize: 37904
[startup+500.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 9082 0 0 0 49980 26 0 0 25 0 1 0 481676655 39206912 8711 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9572 8711 603 41 0 9531 0
vsize: 38288
[startup+510.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 9148 0 0 0 50980 26 0 0 25 0 1 0 481676655 39473152 8777 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9637 8777 603 41 0 9596 0
vsize: 38548
[startup+520.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 9241 0 0 0 51980 26 0 0 25 0 1 0 481676655 40161280 8870 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9805 8870 603 41 0 9764 0
vsize: 39220
[startup+530.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 9331 0 0 0 52981 26 0 0 25 0 1 0 481676655 40431616 8960 4294967295 134512640 134672761 3221224576 3221223680 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9871 8960 603 41 0 9830 0
vsize: 39484
[startup+540.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 9415 0 0 0 53980 27 0 0 25 0 1 0 481676655 40820736 9044 4294967295 134512640 134672761 3221224576 3221223724 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9966 9044 603 41 0 9925 0
vsize: 39864
[startup+550.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 9495 0 0 0 54980 27 0 0 25 0 1 0 481676655 41086976 9124 4294967295 134512640 134672761 3221224576 3221223744 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10031 9124 603 41 0 9990 0
vsize: 40124
[startup+560.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 9575 0 0 0 55980 27 0 0 25 0 1 0 481676655 41484288 9204 4294967295 134512640 134672761 3221224576 3221223728 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10128 9204 603 41 0 10087 0
vsize: 40512
[startup+570.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 9658 0 0 0 56980 28 0 0 25 0 1 0 481676655 41746432 9287 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10192 9287 603 41 0 10151 0
vsize: 40768
[startup+580.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 9734 0 0 0 57980 28 0 0 25 0 1 0 481676655 42143744 9363 4294967295 134512640 134672761 3221224576 3221223712 134560613 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10289 9363 603 41 0 10248 0
vsize: 41156
[startup+590.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 9811 0 0 0 58980 28 0 0 25 0 1 0 481676655 42409984 9440 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10354 9440 603 41 0 10313 0
vsize: 41416
[startup+600.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 9890 0 0 0 59980 29 0 0 25 0 1 0 481676655 42672128 9519 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10418 9519 603 41 0 10377 0
vsize: 41672
[startup+610.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 9964 0 0 0 60979 29 0 0 25 0 1 0 481676655 43065344 9593 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10514 9593 603 41 0 10473 0
vsize: 42056
[startup+620.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 10051 0 0 0 61979 29 0 0 25 0 1 0 481676655 43331584 9680 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10579 9680 603 41 0 10538 0
vsize: 42316
[startup+630.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 10128 0 0 0 62980 29 0 0 25 0 1 0 481676655 43724800 9757 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10675 9757 603 41 0 10634 0
vsize: 42700
[startup+640.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 10226 0 0 0 63980 29 0 0 25 0 1 0 481676655 44126208 9855 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10773 9855 603 41 0 10732 0
vsize: 43092
[startup+650.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 10314 0 0 0 64979 30 0 0 25 0 1 0 481676655 44523520 9943 4294967295 134512640 134672761 3221224576 3221223744 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10870 9943 603 41 0 10829 0
vsize: 43480
[startup+660.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 10396 0 0 0 65979 30 0 0 25 0 1 0 481676655 44789760 10025 4294967295 134512640 134672761 3221224576 3221223740 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10935 10025 603 41 0 10894 0
vsize: 43740
[startup+670.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 10458 0 0 0 66980 30 0 0 25 0 1 0 481676655 45056000 10087 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11000 10087 603 41 0 10959 0
vsize: 44000
[startup+680.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 10520 0 0 0 67979 31 0 0 25 0 1 0 481676655 45326336 10149 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11066 10149 603 41 0 11025 0
vsize: 44264
[startup+690.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 10572 0 0 0 68977 31 0 0 25 0 1 0 481676655 45461504 10201 4294967295 134512640 134672761 3221224576 3221223680 134560025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11099 10201 603 41 0 11058 0
vsize: 44396
[startup+700.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 10631 0 0 0 69977 32 0 0 25 0 1 0 481676655 45727744 10260 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11164 10260 603 41 0 11123 0
vsize: 44656
[startup+710.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 10687 0 0 0 70977 32 0 0 25 0 1 0 481676655 45985792 10316 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11227 10316 603 41 0 11186 0
vsize: 44908
[startup+720.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 10744 0 0 0 71977 32 0 0 25 0 1 0 481676655 46247936 10373 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11291 10373 603 41 0 11250 0
vsize: 45164
[startup+730.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 10803 0 0 0 72977 32 0 0 25 0 1 0 481676655 46383104 10432 4294967295 134512640 134672761 3221224576 3221223712 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11324 10432 603 41 0 11283 0
vsize: 45296
[startup+740.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 10863 0 0 0 73977 32 0 0 25 0 1 0 481676655 46645248 10492 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11388 10492 603 41 0 11347 0
vsize: 45552
[startup+750.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 10916 0 0 0 74977 33 0 0 25 0 1 0 481676655 46907392 10545 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11452 10545 603 41 0 11411 0
vsize: 45808
[startup+760.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 10970 0 0 0 75977 33 0 0 25 0 1 0 481676655 47177728 10599 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11518 10599 603 41 0 11477 0
vsize: 46072
[startup+770.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 11023 0 0 0 76977 33 0 0 25 0 1 0 481676655 47308800 10652 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11550 10652 603 41 0 11509 0
vsize: 46200
[startup+780.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 11079 0 0 0 77977 33 0 0 25 0 1 0 481676655 47570944 10708 4294967295 134512640 134672761 3221224576 3221223744 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11614 10708 603 41 0 11573 0
vsize: 46456
[startup+790.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 11137 0 0 0 78976 34 0 0 25 0 1 0 481676655 47833088 10766 4294967295 134512640 134672761 3221224576 3221223760 134559540 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11678 10767 603 41 0 11637 0
vsize: 46712
[startup+800.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 11184 0 0 0 79977 34 0 0 25 0 1 0 481676655 47964160 10813 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11710 10813 603 41 0 11669 0
vsize: 46840
[startup+810.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 11247 0 0 0 80977 34 0 0 25 0 1 0 481676655 48230400 10876 4294967295 134512640 134672761 3221224576 3221223712 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11775 10876 603 41 0 11734 0
vsize: 47100
[startup+820.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 11312 0 0 0 81977 34 0 0 25 0 1 0 481676655 48496640 10941 4294967295 134512640 134672761 3221224576 3221223744 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11840 10941 603 41 0 11799 0
vsize: 47360
[startup+830.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 11367 0 0 0 82976 34 0 0 25 0 1 0 481676655 48758784 10996 4294967295 134512640 134672761 3221224576 3221223744 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11904 10996 603 41 0 11863 0
vsize: 47616
[startup+840.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 11419 0 0 0 83977 34 0 0 25 0 1 0 481676655 48893952 11048 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11937 11048 603 41 0 11896 0
vsize: 47748
[startup+850.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 11469 0 0 0 84976 35 0 0 25 0 1 0 481676655 49156096 11098 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12001 11098 603 41 0 11960 0
vsize: 48004
[startup+860.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 11530 0 0 0 85977 35 0 0 25 0 1 0 481676655 49434624 11159 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12069 11159 603 41 0 12028 0
vsize: 48276
[startup+870.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 11572 0 0 0 86976 35 0 0 25 0 1 0 481676655 49565696 11201 4294967295 134512640 134672761 3221224576 3221223680 134555251 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12101 11201 603 41 0 12060 0
vsize: 48404
[startup+880.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 11624 0 0 0 87976 36 0 0 25 0 1 0 481676655 49827840 11253 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12165 11253 603 41 0 12124 0
vsize: 48660
[startup+890.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 11680 0 0 0 88976 36 0 0 25 0 1 0 481676655 49958912 11309 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12197 11309 603 41 0 12156 0
vsize: 48788
[startup+900.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 11748 0 0 0 89977 36 0 0 25 0 1 0 481676655 50229248 11377 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12263 11377 603 41 0 12222 0
vsize: 49052
[startup+910.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 11794 0 0 0 90977 36 0 0 25 0 1 0 481676655 50491392 11423 4294967295 134512640 134672761 3221224576 3221223744 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12327 11423 603 41 0 12286 0
vsize: 49308
[startup+920.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 11842 0 0 0 91977 36 0 0 25 0 1 0 481676655 50622464 11471 4294967295 134512640 134672761 3221224576 3221223680 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12359 11471 603 41 0 12318 0
vsize: 49436
[startup+930.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 11889 0 0 0 92977 36 0 0 25 0 1 0 481676655 50896896 11518 4294967295 134512640 134672761 3221224576 3221223724 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12426 11518 603 41 0 12385 0
vsize: 49704
[startup+940.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 11941 0 0 0 93977 36 0 0 25 0 1 0 481676655 51027968 11570 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12458 11570 603 41 0 12417 0
vsize: 49832
[startup+950.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 11986 0 0 0 94977 37 0 0 25 0 1 0 481676655 51290112 11615 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12522 11615 603 41 0 12481 0
vsize: 50088
[startup+960.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 12037 0 0 0 95977 37 0 0 25 0 1 0 481676655 51421184 11666 4294967295 134512640 134672761 3221224576 3221223712 134560686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12554 11666 603 41 0 12513 0
vsize: 50216
[startup+970.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 12081 0 0 0 96976 37 0 0 25 0 1 0 481676655 51687424 11710 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12619 11710 603 41 0 12578 0
vsize: 50476
[startup+980.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 12138 0 0 0 97976 38 0 0 25 0 1 0 481676655 51818496 11767 4294967295 134512640 134672761 3221224576 3221223760 134558557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12651 11767 603 41 0 12610 0
vsize: 50604
[startup+990.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 12194 0 0 0 98976 38 0 0 25 0 1 0 481676655 52092928 11823 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12718 11823 603 41 0 12677 0
vsize: 50872
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 12248 0 0 0 99976 38 0 0 25 0 1 0 481676655 52355072 11877 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12782 11877 603 41 0 12741 0
vsize: 51128
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 12306 0 0 0 100976 38 0 0 25 0 1 0 481676655 52633600 11935 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12850 11935 603 41 0 12809 0
vsize: 51400
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 12367 0 0 0 101976 38 0 0 25 0 1 0 481676655 52768768 11996 4294967295 134512640 134672761 3221224576 3221223712 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12883 11996 603 41 0 12842 0
vsize: 51532
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 12423 0 0 0 102976 39 0 0 25 0 1 0 481676655 53030912 12052 4294967295 134512640 134672761 3221224576 3221223680 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12947 12052 603 41 0 12906 0
vsize: 51788
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 12477 0 0 0 103975 39 0 0 25 0 1 0 481676655 53334016 12106 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13021 12106 603 41 0 12980 0
vsize: 52084
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 12528 0 0 0 104976 39 0 0 25 0 1 0 481676655 53465088 12157 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13053 12157 603 41 0 13012 0
vsize: 52212
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 12586 0 0 0 105976 39 0 0 25 0 1 0 481676655 53731328 12215 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13118 12215 603 41 0 13077 0
vsize: 52472
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 12645 0 0 0 106975 40 0 0 25 0 1 0 481676655 53993472 12274 4294967295 134512640 134672761 3221224576 3221223744 134561261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13182 12274 603 41 0 13141 0
vsize: 52728
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 12703 0 0 0 107975 40 0 0 25 0 1 0 481676655 54128640 12332 4294967295 134512640 134672761 3221224576 3221223728 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13215 12332 603 41 0 13174 0
vsize: 52860
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 12752 0 0 0 108975 40 0 0 25 0 1 0 481676655 54394880 12381 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13280 12381 603 41 0 13239 0
vsize: 53120
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 12797 0 0 0 109975 40 0 0 25 0 1 0 481676655 54591488 12426 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13328 12426 603 41 0 13287 0
vsize: 53312
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 12843 0 0 0 110976 40 0 0 25 0 1 0 481676655 54853632 12472 4294967295 134512640 134672761 3221224576 3221223712 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13392 12472 603 41 0 13351 0
vsize: 53568
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 12883 0 0 0 111976 40 0 0 25 0 1 0 481676655 54984704 12512 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13424 12512 603 41 0 13383 0
vsize: 53696
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 12927 0 0 0 112976 41 0 0 25 0 1 0 481676655 55115776 12556 4294967295 134512640 134672761 3221224576 3221223744 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13456 12556 603 41 0 13415 0
vsize: 53824
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 12978 0 0 0 113976 41 0 0 25 0 1 0 481676655 55382016 12607 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13521 12607 603 41 0 13480 0
vsize: 54084
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 13026 0 0 0 114976 41 0 0 25 0 1 0 481676655 55541760 12655 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13560 12655 603 41 0 13519 0
vsize: 54240
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 13065 0 0 0 115976 41 0 0 25 0 1 0 481676655 55672832 12694 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13592 12694 603 41 0 13551 0
vsize: 54368
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 13111 0 0 0 116976 41 0 0 25 0 1 0 481676655 55975936 12740 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13666 12740 603 41 0 13625 0
vsize: 54664
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 13159 0 0 0 117976 41 0 0 25 0 1 0 481676655 56111104 12788 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13699 12788 603 41 0 13658 0
vsize: 54796
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 13209 0 0 0 118976 41 0 0 25 0 1 0 481676655 56385536 12838 4294967295 134512640 134672761 3221224576 3221223680 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13766 12838 603 41 0 13725 0
vsize: 55064
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25120
Raw data (stat): 25120 (minisat+) R 25119 18865 18864 0 -1 0 13254 0 0 0 119976 41 0 0 25 0 1 0 481676655 56516608 12883 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13798 12883 603 41 0 13757 0
vsize: 55192
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 25120
Raw data (stat): 25120 (minisat+) Z 25119 18865 18864 0 -1 12 13257 0 0 0 119976 44 0 0 25 0 1 0 481676655 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.07
CPU time (s): 1200.21
CPU user time (s): 1199.77
CPU system time (s): 0.441932
CPU usage (%): 100.012
Max. virtual memory (Kb): 55192
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####