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-ii8b2.opb
MD5SUM	bbfcebd70586668574286ad19a1cd5a8
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	379
Optimality of the best value was proved	NO
Number of terms in the objective function	1152
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	1152
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	1152
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.03984
Number of variables	1152
Total number of constraints	4664
Number of constraints which are clauses	4664
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	8
Trace number 31577

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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:        854292 kB
Buffers:         32860 kB
Cached:         126776 kB
SwapCached:        640 kB
Active:          47940 kB
Inactive:       113788 kB
HighTotal:      131008 kB
HighFree:        25144 kB
LowTotal:       903652 kB
LowFree:        829148 kB
SwapTotal:     2097136 kB
SwapFree:      2095632 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5108 kB
Slab:            12988 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-27 05:15:46 (client local time) WITH STATUS 152 IN 1229.86 SECONDS
stats: 22922 7 1229.86 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 4664 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 |    4664    10368 |    1554       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 418[0m
c ---[   0]---> Sorter-cost:63108     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         4 |   80342   187277 |   26780       4       53    13.2 |  0.000 % |
c |       105 |   80295   187182 |   29458     103     4570    44.4 |  0.068 % |
c |       255 |   80295   187182 |   32403     253    11493    45.4 |  0.068 % |
c |       480 |   78340   182905 |   35644     415    22935    55.3 |  2.335 % |
c |       818 |   78287   182784 |   39208     750    30890    41.2 |  2.402 % |
c |      1325 |   78287   182784 |   43129    1257    74531    59.3 |  2.402 % |
c |      2085 |   78203   182602 |   47442    2015   104674    51.9 |  2.498 % |
c ==============================================================================
c [1mFound solution: 395[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2395 |   78562   183587 |   26187    2325   119226    51.3 |  2.498 % |
c |      2496 |   78562   183587 |   28805    2426   120994    49.9 |  2.488 % |
c |      2646 |   78562   183587 |   31686    2576   125847    48.9 |  2.488 % |
c |      2871 |   78562   183587 |   34854    2801   133995    47.8 |  2.488 % |
c |      3208 |   78499   183450 |   38340    3137   143848    45.9 |  2.560 % |
c |      3716 |   77783   181858 |   42174    3570   162643    45.6 |  3.412 % |
c |      4476 |   77760   181811 |   46391    4139   190783    46.1 |  3.433 % |
c |      5616 |   77632   181541 |   51031    5272   314876    59.7 |  3.567 % |
c |      7324 |   77587   181446 |   56134    6979   364272    52.2 |  3.616 % |
c |      9888 |   77395   181025 |   61747    9516   439997    46.2 |  3.836 % |
c |     13733 |   77233   180675 |   67922   13357   771030    57.7 |  4.014 % |
c ==============================================================================
c [1mFound solution: 387[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17494 |   77317   180956 |   25772   17111   909290    53.1 |  4.014 % |
c |     17594 |   77317   180956 |   28349   17211   912798    53.0 |  4.079 % |
c |     17745 |   77301   180922 |   31184   17359   917832    52.9 |  4.097 % |
c |     17971 |   77301   180922 |   34302   17585   922741    52.5 |  4.097 % |
c |     18308 |   77301   180922 |   37732   17922   975464    54.4 |  4.097 % |
c |     18814 |   77000   180271 |   41506   18420   993851    54.0 |  4.430 % |
c ==============================================================================
c [1mFound solution: 384[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19542 |   76949   180180 |   25649   19073   997675    52.3 |  4.430 % |
c |     19642 |   76949   180180 |   28213   19173   999183    52.1 |  4.567 % |
c |     19792 |   76949   180180 |   31035   19323  1005573    52.0 |  4.567 % |
c |     20017 |   76865   179998 |   34138   19456  1010930    52.0 |  4.660 % |
c |     20354 |   76865   179998 |   37552   19793  1041428    52.6 |  4.660 % |
c |     20860 |   76865   179998 |   41307   20299  1059829    52.2 |  4.660 % |
c |     21619 |   76831   179926 |   45438   20274  1068528    52.7 |  4.697 % |
c |     22759 |   76831   179926 |   49982   21414  1107610    51.7 |  4.697 % |
c |     24468 |   76805   179864 |   54980   23097  1204602    52.2 |  4.732 % |
c |     27030 |   76805   179864 |   60479   25659  1423323    55.5 |  4.732 % |
c |     30876 |   76805   179864 |   66526   29505  1560456    52.9 |  4.732 % |
c |     36642 |   76805   179864 |   73179   35271  2075604    58.8 |  4.732 % |
c |     45292 |   76805   179864 |   80497   43921  2991534    68.1 |  4.732 % |
c ==============================================================================
c [1mFound solution: 380[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     57655 |   76754   179790 |   25584   55821  4052834    72.6 |  4.732 % |
c |     57755 |   76754   179790 |   28142   18665  1212846    65.0 |  4.881 % |
c |     57905 |   76754   179790 |   30956   18815  1221408    64.9 |  4.881 % |
c |     58132 |   76754   179790 |   34052   19042  1230212    64.6 |  4.881 % |
c |     58469 |   76691   179657 |   37457   19378  1238118    63.9 |  4.949 % |
c |     58975 |   76691   179657 |   41203   19884  1286725    64.7 |  4.949 % |
c |     59734 |   76637   179539 |   45323   20642  1347364    65.3 |  5.011 % |
c |     60874 |   76635   179535 |   49855   21781  1441910    66.2 |  5.013 % |
c |     62582 |   76635   179535 |   54841   23489  1579487    67.2 |  5.013 % |
c |     65147 |   76592   179438 |   60325   26053  1740507    66.8 |  5.063 % |
c |     68991 |   76592   179438 |   66358   29897  2141648    71.6 |  5.063 % |
c |     74758 |   76592   179438 |   72994   35664  2591073    72.7 |  5.063 % |
c |     83407 |   76592   179438 |   80293   44313  3254447    73.4 |  5.063 % |
c |     96381 |   76550   179348 |   88322   57274  4197372    73.3 |  5.108 % |
c |    115843 |   76550   179348 |   97155   76736  5614266    73.2 |  5.108 % |
c |    145036 |   76550   179348 |  106870  105929  7745460    73.1 |  5.108 % |
/oldhome/oroussel/solvers/minisat+_script: line 9:   473 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.91 0.95 0.88 2/54 469
Raw data (stat): 469 (runsolver) R 468 7266 7265 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 795222044 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.0001 s]
Raw data (loadavg): 0.93 0.95 0.88 2/55 473
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0007 s]
Raw data (loadavg): 0.94 0.96 0.88 2/55 473
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0014 s]
Raw data (loadavg): 0.95 0.96 0.88 2/55 473
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0027 s]
Raw data (loadavg): 0.95 0.96 0.88 2/55 473
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0033 s]
Raw data (loadavg): 0.96 0.96 0.88 2/55 473
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0028 s]
Raw data (loadavg): 0.97 0.96 0.89 2/55 473
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0043 s]
Raw data (loadavg): 0.97 0.96 0.89 2/55 473
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0048 s]
Raw data (loadavg): 0.98 0.96 0.89 2/55 473
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0053 s]
Raw data (loadavg): 0.98 0.96 0.89 2/55 473
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.006 s]
Raw data (loadavg): 0.98 0.96 0.89 2/55 473
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.006 s]
Raw data (loadavg): 0.98 0.96 0.89 2/55 473
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.007 s]
Raw data (loadavg): 0.99 0.97 0.89 2/55 473
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.007 s]
Raw data (loadavg): 0.99 0.97 0.89 2/55 473
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.008 s]
Raw data (loadavg): 0.99 0.97 0.89 2/55 473
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.008 s]
Raw data (loadavg): 0.99 0.97 0.89 2/55 473
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.009 s]
Raw data (loadavg): 0.99 0.97 0.89 2/55 473
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.01 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 473
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.01 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 473
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.011 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 473
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.012 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 473
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.012 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 473
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.013 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 473
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.013 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 473
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.013 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 473
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.014 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 473
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.015 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 473
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 473
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 473
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.2 s]
Raw data (loadavg): 0.99 0.97 0.91 3/58 509
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.201 s]
Raw data (loadavg): 1.15 1.00 0.92 2/55 526
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.2 s]
Raw data (loadavg): 1.12 1.00 0.92 2/55 526
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.315 s]
Raw data (loadavg): 1.10 1.00 0.92 2/55 526
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.315 s]
Raw data (loadavg): 1.09 1.00 0.92 2/55 526
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.316 s]
Raw data (loadavg): 1.07 1.00 0.92 2/55 526
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.316 s]
Raw data (loadavg): 1.06 1.00 0.92 2/55 526
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.316 s]
Raw data (loadavg): 1.05 1.00 0.92 2/55 526
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.317 s]
Raw data (loadavg): 1.04 1.00 0.92 2/55 528
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.317 s]
Raw data (loadavg): 1.04 1.00 0.92 2/55 528
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.317 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 528
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.318 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 528
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.318 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 528
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.318 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 528
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.318 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 528
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.32 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 528
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.32 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 528
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.321 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 528
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.321 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 528
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.321 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 528
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.321 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 528
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.322 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 528
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.321 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 528
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.322 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 528
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.322 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 528
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.323 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 528
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.323 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 528
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.324 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 528
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.324 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 528
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.324 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 528
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.325 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 528
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.325 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 528
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.324 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 528
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.326 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 528
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.326 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.325 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.325 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.325 s]
Raw data (loadavg): 1.07 1.02 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.326 s]
Raw data (loadavg): 1.06 1.02 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.326 s]
Raw data (loadavg): 1.05 1.01 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.326 s]
Raw data (loadavg): 1.04 1.01 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.326 s]
Raw data (loadavg): 1.04 1.01 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.326 s]
Raw data (loadavg): 1.03 1.01 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.326 s]
Raw data (loadavg): 1.02 1.01 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.326 s]
Raw data (loadavg): 1.02 1.01 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.326 s]
Raw data (loadavg): 1.02 1.01 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.326 s]
Raw data (loadavg): 1.01 1.01 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.326 s]
Raw data (loadavg): 1.01 1.01 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.327 s]
Raw data (loadavg): 1.01 1.01 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.326 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.327 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.327 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.327 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.327 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.327 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.327 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.327 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.327 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.328 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.328 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.327 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.328 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.328 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.329 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.328 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.328 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.329 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.329 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.33 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.33 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.329 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.33 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.33 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.33 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.33 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.33 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.33 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.33 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.33 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.33 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.33 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.33 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.33 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.33 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.33 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.33 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.33 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.33 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.33 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.33 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.33 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.33 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.33 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.33 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.73 s]
Raw data (loadavg): 1.00 1.00 0.92 1/53 530
Raw data (stat): 469 (minisat+_script) S 468 7266 7265 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795222044 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

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