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/primes-dimacs-cnf/normalized-ii8e1.opb
MD5SUM	979ebd144bbd2b562b23479b90a02c66
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	343
Optimality of the best value was proved	NO
Number of terms in the objective function	1040
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	1040
Number of bits of the sum of numbers in the objective function	11
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	1040
Number of bits of the biggest sum of numbers	11
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03484
Number of variables	1040
Total number of constraints	3656
Number of constraints which are clauses	3656
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	10
Trace number 31586

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc19 THE 2005-05-27 04:56:45 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22929 boxname=wulflinc19 idbench=175 idsolver=16 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  979ebd144bbd2b562b23479b90a02c66  /oldhome/oroussel/tmp/wulflinc19/normalized-ii8e1.opb
REAL COMMAND:  minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc19/normalized-ii8e1.opb
IDLAUNCH: 22929
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        844344 kB
Buffers:         33216 kB
Cached:         131200 kB
SwapCached:        756 kB
Active:          51604 kB
Inactive:       115128 kB
HighTotal:      131008 kB
HighFree:        63644 kB
LowTotal:       903652 kB
LowFree:        780700 kB
SwapTotal:     2097892 kB
SwapFree:      2096428 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5420 kB
Slab:            17944 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-27 05:17:15 (client local time) WITH STATUS 152 IN 1229.86 SECONDS
stats: 22929 7 1229.86 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 3656 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 |    3656     8440 |    1218       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 474[0m
c ---[   0]---> Sorter-cost:56938     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        16 |   70910   165682 |   23636      16      122     7.6 |  0.000 % |
c |       116 |   70460   164722 |   25999     103     1702    16.5 |  0.584 % |
c |       266 |   70366   164520 |   28599     251     3649    14.5 |  0.702 % |
c ==============================================================================
c [1mFound solution: 440[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       324 |   70706   165477 |   23568     308     4715    15.3 |  0.702 % |
c |       424 |   70706   165477 |   25924     408     8292    20.3 |  0.881 % |
c |       574 |   70653   165366 |   28517     557    11419    20.5 |  0.944 % |
c |       799 |   70277   164548 |   31369     774    16815    21.7 |  1.426 % |
c |      1136 |   69825   163548 |   34505    1101    24172    22.0 |  2.023 % |
c |      1642 |   69406   162625 |   37956    1599    30670    19.2 |  2.572 % |
c ==============================================================================
c [1mFound solution: 429[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1886 |   69590   163152 |   23196    1843    55930    30.3 |  2.572 % |
c |      1986 |   69306   162524 |   25515    1937    57229    29.5 |  2.942 % |
c |      2136 |   69079   162021 |   28067    2083    61357    29.5 |  3.242 % |
c |      2361 |   68171   160009 |   30873    2287    67394    29.5 |  4.442 % |
c |      2698 |   68059   159757 |   33961    2621    70752    27.0 |  4.594 % |
c |      3208 |   67945   159503 |   37357    3128    87704    28.0 |  4.747 % |
c |      3967 |   67209   157861 |   41093    3861   122114    31.6 |  5.729 % |
c ==============================================================================
c [1mFound solution: 414[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4195 |   67146   157822 |   22382    3999   111918    28.0 |  5.729 % |
c |      4297 |   67146   157822 |   24620    4101   113775    27.7 |  6.062 % |
c |      4447 |   67146   157822 |   27082    4251   118820    28.0 |  6.062 % |
c |      4672 |   67146   157822 |   29790    4476   123841    27.7 |  6.062 % |
c |      5009 |   67081   157679 |   32769    4807   132551    27.6 |  6.147 % |
c ==============================================================================
c [1mFound solution: 362[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5342 |   67696   159233 |   22565    5140   138591    27.0 |  6.147 % |
c |      5442 |   67696   159233 |   24821    5240   141150    26.9 |  6.121 % |
c |      5592 |   67574   158961 |   27303    5384   146685    27.2 |  6.283 % |
c |      5817 |   67381   158536 |   30034    5589   156968    28.1 |  6.530 % |
c |      6155 |   67381   158536 |   33037    5927   164294    27.7 |  6.530 % |
c |      6661 |   67381   158536 |   36341    6433   187592    29.2 |  6.530 % |
c |      7420 |   67381   158536 |   39975    7192   215762    30.0 |  6.530 % |
c |      8560 |   67291   158326 |   43972    8294   284482    34.3 |  6.659 % |
c |     10270 |   67291   158326 |   48370   10004   414845    41.5 |  6.659 % |
c |     12833 |   67291   158326 |   53207   12567   524495    41.7 |  6.659 % |
c |     16678 |   67135   157972 |   58527   16360   743881    45.5 |  6.871 % |
c |     22446 |   67135   157972 |   64380   22128  1273293    57.5 |  6.871 % |
c |     31095 |   67135   157972 |   70818   30777  1993596    64.8 |  6.871 % |
c |     44070 |   67037   157760 |   77900   43749  3626738    82.9 |  6.992 % |
c |     63531 |   66978   157633 |   85690   63190  7217145   114.2 |  7.065 % |
c ==============================================================================
c [1mFound solution: 357[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     76928 |   67082   157937 |   22360   76587  9369778   122.3 |  7.065 % |
c |     77028 |   67082   157937 |   24596   14758  2105104   142.6 |  7.063 % |
c |     77179 |   67082   157937 |   27055   14909  2113234   141.7 |  7.063 % |
c |     77404 |   66929   157594 |   29761   15123  2117648   140.0 |  7.267 % |
c |     77741 |   66893   157516 |   32737   15450  2132379   138.0 |  7.312 % |
c |     78249 |   66893   157516 |   36011   15958  2160898   135.4 |  7.312 % |
c |     79009 |   66855   157432 |   39612   16717  2198342   131.5 |  7.359 % |
c |     80148 |   66855   157432 |   43573   17856  2287067   128.1 |  7.359 % |
c |     81856 |   66855   157432 |   47930   19564  2321382   118.7 |  7.359 % |
c |     84420 |   66532   156717 |   52723   19452  2371382   121.9 |  7.775 % |
c |     88265 |   66529   156710 |   57996   23294  2666932   114.5 |  7.779 % |
c |     94033 |   66529   156710 |   63795   29062  2976594   102.4 |  7.779 % |
c |    102683 |   66529   156710 |   70175   37712  3416974    90.6 |  7.779 % |
c |    115658 |   66529   156710 |   77192   50687  4427403    87.3 |  7.779 % |
c |    135119 |   66529   156710 |   84912   70148  6596312    94.0 |  7.779 % |
c |    164312 |   66529   156710 |   93403   29360  1609564    54.8 |  7.779 % |
c |    208101 |   66529   156710 |  102743   73149  7115278    97.3 |  7.779 % |
/oldhome/oroussel/solvers/minisat+_script: line 9:   873 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### 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.97 0.89 2/54 869
Raw data (stat): 869 (runsolver) R 868 10795 10794 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 853444946 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 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.0009 s]
Raw data (loadavg): 0.93 0.97 0.89 2/55 873
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0012 s]
Raw data (loadavg): 0.94 0.97 0.89 2/55 873
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0011 s]
Raw data (loadavg): 0.95 0.97 0.89 2/55 873
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0009 s]
Raw data (loadavg): 0.96 0.97 0.89 2/55 873
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0011 s]
Raw data (loadavg): 0.96 0.97 0.89 2/55 873
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0017 s]
Raw data (loadavg): 0.97 0.97 0.89 2/55 873
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0019 s]
Raw data (loadavg): 0.97 0.97 0.89 2/55 873
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0017 s]
Raw data (loadavg): 0.98 0.97 0.89 2/55 873
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0022 s]
Raw data (loadavg): 0.98 0.97 0.89 2/55 873
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.002 s]
Raw data (loadavg): 0.98 0.97 0.90 2/55 873
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.003 s]
Raw data (loadavg): 0.98 0.97 0.90 2/55 873
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.003 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 873
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 873
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 873
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.003 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 873
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 873
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 873
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 873
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 873
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.008 s]
Raw data (loadavg): 1.07 0.99 0.91 2/56 874
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.008 s]
Raw data (loadavg): 1.22 1.02 0.92 2/59 916
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.008 s]
Raw data (loadavg): 1.26 1.04 0.93 2/55 926
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.041 s]
Raw data (loadavg): 1.22 1.03 0.93 2/55 926
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.041 s]
Raw data (loadavg): 1.18 1.03 0.93 2/55 926
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.042 s]
Raw data (loadavg): 1.15 1.03 0.93 2/55 926
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.042 s]
Raw data (loadavg): 1.13 1.03 0.93 2/55 926
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.042 s]
Raw data (loadavg): 1.11 1.03 0.93 2/55 926
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.042 s]
Raw data (loadavg): 1.09 1.03 0.93 2/55 928
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.042 s]
Raw data (loadavg): 1.08 1.03 0.93 2/55 928
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.042 s]
Raw data (loadavg): 1.07 1.02 0.93 2/55 928
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.042 s]
Raw data (loadavg): 1.06 1.02 0.93 2/55 928
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.044 s]
Raw data (loadavg): 1.05 1.02 0.93 2/55 928
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.043 s]
Raw data (loadavg): 1.04 1.02 0.93 2/55 928
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.043 s]
Raw data (loadavg): 1.03 1.02 0.93 2/55 928
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.043 s]
Raw data (loadavg): 1.03 1.02 0.93 2/55 928
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.044 s]
Raw data (loadavg): 1.02 1.02 0.93 2/55 928
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.043 s]
Raw data (loadavg): 1.02 1.02 0.93 2/55 928
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.043 s]
Raw data (loadavg): 1.02 1.02 0.93 2/55 928
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.044 s]
Raw data (loadavg): 1.01 1.02 0.93 2/55 928
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.044 s]
Raw data (loadavg): 1.01 1.01 0.93 2/55 928
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.044 s]
Raw data (loadavg): 1.01 1.01 0.93 2/55 928
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.045 s]
Raw data (loadavg): 1.01 1.01 0.93 2/55 928
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.044 s]
Raw data (loadavg): 1.00 1.01 0.93 2/55 928
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.044 s]
Raw data (loadavg): 1.00 1.01 0.93 2/55 928
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.045 s]
Raw data (loadavg): 1.00 1.01 0.93 2/55 928
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.045 s]
Raw data (loadavg): 1.00 1.01 0.93 2/55 928
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.045 s]
Raw data (loadavg): 1.00 1.01 0.93 2/55 928
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.045 s]
Raw data (loadavg): 1.00 1.01 0.93 2/55 928
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.045 s]
Raw data (loadavg): 1.00 1.01 0.93 2/55 928
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.045 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 928
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.046 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 928
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.047 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 928
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.047 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 928
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.048 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 928
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.047 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 928
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.048 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 928
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.048 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 928
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.048 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 928
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.049 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.049 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.049 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.049 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.049 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.049 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.049 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.051 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.051 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.052 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.051 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.051 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.052 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.051 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.051 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.054 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.054 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.055 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.056 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.056 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.056 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.056 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.057 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.058 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.059 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.059 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.059 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.061 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.062 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.061 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.061 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.062 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.062 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.063 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.064 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.063 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.064 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.72 s]
Raw data (loadavg): 1.00 1.00 0.93 1/53 930
Raw data (stat): 869 (minisat+_script) S 868 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853444946 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.72
CPU time (s): 1229.86
CPU user time (s): 1229.25
CPU system time (s): 0.608907
CPU usage (%): 100.011
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####