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/logic-synthesis/normalized-e64.b.opb
MD5SUM	bf7f8537c6faa135d25c67c53576abb5
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	49
Optimality of the best value was proved	NO
Number of terms in the objective function	608
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	608
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	608
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03484
Number of variables	607
Total number of constraints	1053
Number of constraints which are clauses	1022
Number of constraints which are cardinality constraints (but not clauses)	31
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	3
Maximum length of a constraint	32
Trace number 31488

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc23 THE 2005-05-27 04:34:38 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22820 boxname=wulflinc23 idbench=66 idsolver=16 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  bf7f8537c6faa135d25c67c53576abb5  /oldhome/oroussel/tmp/wulflinc23/normalized-e64.b.opb
REAL COMMAND:  minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc23/normalized-e64.b.opb
IDLAUNCH: 22820
/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:        457940 kB
Buffers:         33808 kB
Cached:         521016 kB
SwapCached:        532 kB
Active:          44688 kB
Inactive:       512480 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        457688 kB
SwapTotal:     2097136 kB
SwapFree:      2096016 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5636 kB
Slab:            13860 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-27 04:55:08 (client local time) WITH STATUS 152 IN 1229.85 SECONDS
stats: 22820 7 1229.85 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1022 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 |    1022     8200 |     340       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 82[0m
c ---[   0]---> Sorter-cost:27428     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         1 |   32888    82605 |   10962       1       16    16.0 |  0.000 % |
c |       101 |   32731    82280 |   12058      94     1328    14.1 |  0.441 % |
c |       251 |   32731    82280 |   13264     244     4888    20.0 |  0.441 % |
c |       476 |   32693    82200 |   14590     467     9207    19.7 |  0.538 % |
c |       815 |   32655    82120 |   16049     805    14538    18.1 |  0.636 % |
c ==============================================================================
c [1mFound solution: 64[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1118 |   32544    81867 |   10848    1108    20015    18.1 |  0.636 % |
c |      1219 |   32544    81867 |   11932    1209    21890    18.1 |  1.342 % |
c |      1371 |   32544    81867 |   13126    1361    27251    20.0 |  1.342 % |
c |      1597 |   32544    81867 |   14438    1587    32001    20.2 |  1.342 % |
c |      1935 |   32544    81867 |   15882    1925    44062    22.9 |  1.342 % |
c |      2442 |   32526    81825 |   17470    2426    58440    24.1 |  1.397 % |
c |      3201 |   32524    81821 |   19217    3182    81772    25.7 |  1.402 % |
c |      4340 |   32524    81821 |   21139    4321   124438    28.8 |  1.402 % |
c |      6049 |   32524    81821 |   23253    6030   236669    39.2 |  1.402 % |
c |      8611 |   32524    81821 |   25579    8592   404633    47.1 |  1.402 % |
c |     12456 |   32524    81821 |   28136   12437   881628    70.9 |  1.402 % |
c ==============================================================================
c [1mFound solution: 57[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17530 |   32583    81971 |   10861   17511  1261267    72.0 |  1.402 % |
c |     17631 |   32583    81971 |   11947    8857   728551    82.3 |  1.404 % |
c |     17781 |   32557    81915 |   13141    9005   733381    81.4 |  1.474 % |
c |     18007 |   32557    81915 |   14455    9231   741448    80.3 |  1.474 % |
c |     18344 |   32557    81915 |   15901    9568   749366    78.3 |  1.474 % |
c |     18850 |   32557    81915 |   17491   10074   785392    78.0 |  1.474 % |
c |     19609 |   32557    81915 |   19240   10833   859333    79.3 |  1.474 % |
c |     20748 |   32557    81915 |   21165   11972   919844    76.8 |  1.474 % |
c |     22458 |   32557    81915 |   23281   13682  1056358    77.2 |  1.474 % |
c |     25020 |   32557    81915 |   25609   16244  1287855    79.3 |  1.474 % |
c ==============================================================================
c [1mFound solution: 55[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25537 |   32576    81969 |   10858   16761  1329272    79.3 |  1.474 % |
c |     25637 |   32576    81969 |   11943    8481   589547    69.5 |  1.477 % |
c |     25787 |   32576    81969 |   13138    8631   595037    68.9 |  1.477 % |
c |     26012 |   32576    81969 |   14451    8856   607205    68.6 |  1.477 % |
c |     26349 |   32576    81969 |   15897    9193   625383    68.0 |  1.477 % |
c |     26855 |   32576    81969 |   17486    9699   645599    66.6 |  1.477 % |
c |     27616 |   32576    81969 |   19235   10460   688721    65.8 |  1.477 % |
c |     28755 |   32576    81969 |   21159   11599   760883    65.6 |  1.477 % |
c |     30463 |   32576    81969 |   23275   13307   926598    69.6 |  1.477 % |
c |     33026 |   32576    81969 |   25602   15870  1052589    66.3 |  1.477 % |
c |     36872 |   32576    81969 |   28162   19716  1313125    66.6 |  1.477 % |
c |     42638 |   32540    81893 |   30979   25472  1707177    67.0 |  1.570 % |
c |     51288 |   32540    81893 |   34077   13453   850735    63.2 |  1.570 % |
c |     64262 |   32540    81893 |   37484   26427  1854535    70.2 |  1.570 % |
c ==============================================================================
c [1mFound solution: 53[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     71120 |   32558    81945 |   10852   33285  2473346    74.3 |  1.570 % |
c |     71222 |   32558    81945 |   11937    6680   548160    82.1 |  1.583 % |
c |     71372 |   32558    81945 |   13130    6830   551418    80.7 |  1.583 % |
c |     71597 |   32558    81945 |   14444    7055   563546    79.9 |  1.583 % |
c |     71934 |   32558    81945 |   15888    7392   572407    77.4 |  1.583 % |
c |     72440 |   32558    81945 |   17477    7898   589289    74.6 |  1.583 % |
c |     73199 |   32558    81945 |   19224    8657   630654    72.8 |  1.583 % |
c |     74340 |   32558    81945 |   21147    9798   684750    69.9 |  1.583 % |
c |     76048 |   32558    81945 |   23262   11506   842785    73.2 |  1.583 % |
c |     78611 |   32558    81945 |   25588   14069  1080790    76.8 |  1.583 % |
c |     82457 |   32558    81945 |   28147   17915  1447445    80.8 |  1.583 % |
c |     88223 |   32558    81945 |   30962   23681  1883985    79.6 |  1.583 % |
c |     96872 |   32558    81945 |   34058   32330  2567295    79.4 |  1.583 % |
c |    109848 |   32558    81945 |   37464   21298  1707483    80.2 |  1.583 % |
c |    129309 |   32558    81945 |   41210   13470  1145174    85.0 |  1.583 % |
c |    158501 |   32558    81945 |   45331   42662  3823977    89.6 |  1.583 % |
c |    202290 |   32558    81945 |   49864   18699  1418328    75.9 |  1.583 % |
c |    267976 |   32558    81945 |   54851   46288  3760997    81.3 |  1.583 % |
c |    366502 |   32558    81945 |   60336   17595  1604710    91.2 |  1.583 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 27022 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.95 0.70 2/54 27018
Raw data (stat): 27018 (runsolver) R 27017 5562 5561 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 853321911 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.93 0.95 0.70 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.0013 s]
Raw data (loadavg): 0.94 0.96 0.70 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.0015 s]
Raw data (loadavg): 0.95 0.96 0.71 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.0016 s]
Raw data (loadavg): 0.96 0.96 0.71 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.1043 s]
Raw data (loadavg): 0.96 0.96 0.71 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.1053 s]
Raw data (loadavg): 0.97 0.96 0.72 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.1075 s]
Raw data (loadavg): 0.97 0.96 0.72 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.1072 s]
Raw data (loadavg): 0.98 0.96 0.72 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.1083 s]
Raw data (loadavg): 0.98 0.96 0.73 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.108 s]
Raw data (loadavg): 0.98 0.96 0.73 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.109 s]
Raw data (loadavg): 0.98 0.96 0.73 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.109 s]
Raw data (loadavg): 0.99 0.97 0.73 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.108 s]
Raw data (loadavg): 0.99 0.97 0.73 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.109 s]
Raw data (loadavg): 0.99 0.97 0.74 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.109 s]
Raw data (loadavg): 0.99 0.97 0.74 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.109 s]
Raw data (loadavg): 0.99 0.97 0.74 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.109 s]
Raw data (loadavg): 0.99 0.97 0.74 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.109 s]
Raw data (loadavg): 0.99 0.97 0.74 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.109 s]
Raw data (loadavg): 0.99 0.97 0.75 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.109 s]
Raw data (loadavg): 0.99 0.97 0.75 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.11 s]
Raw data (loadavg): 0.99 0.97 0.75 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.11 s]
Raw data (loadavg): 0.99 0.97 0.75 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.11 s]
Raw data (loadavg): 0.99 0.97 0.75 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.111 s]
Raw data (loadavg): 0.99 0.97 0.76 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.111 s]
Raw data (loadavg): 0.99 0.97 0.76 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.112 s]
Raw data (loadavg): 0.99 0.97 0.76 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.112 s]
Raw data (loadavg): 0.99 0.97 0.76 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.111 s]
Raw data (loadavg): 0.99 0.97 0.76 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.112 s]
Raw data (loadavg): 0.99 0.97 0.77 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.112 s]
Raw data (loadavg): 0.99 0.97 0.77 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.112 s]
Raw data (loadavg): 0.99 0.97 0.77 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.113 s]
Raw data (loadavg): 0.99 0.97 0.77 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.113 s]
Raw data (loadavg): 0.99 0.97 0.77 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.113 s]
Raw data (loadavg): 0.99 0.97 0.78 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.114 s]
Raw data (loadavg): 0.99 0.97 0.78 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.114 s]
Raw data (loadavg): 0.99 0.97 0.78 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.114 s]
Raw data (loadavg): 0.99 0.97 0.78 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.113 s]
Raw data (loadavg): 0.99 0.97 0.78 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.114 s]
Raw data (loadavg): 0.99 0.97 0.79 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.114 s]
Raw data (loadavg): 0.99 0.97 0.79 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.115 s]
Raw data (loadavg): 0.99 0.97 0.79 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.219 s]
Raw data (loadavg): 0.99 0.97 0.79 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.219 s]
Raw data (loadavg): 0.99 0.97 0.79 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.218 s]
Raw data (loadavg): 0.99 0.97 0.79 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.218 s]
Raw data (loadavg): 0.99 0.97 0.80 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.226 s]
Raw data (loadavg): 0.99 0.97 0.80 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.226 s]
Raw data (loadavg): 0.99 0.97 0.80 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.225 s]
Raw data (loadavg): 0.99 0.97 0.80 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.226 s]
Raw data (loadavg): 0.99 0.97 0.80 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.225 s]
Raw data (loadavg): 0.99 0.97 0.81 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.226 s]
Raw data (loadavg): 0.99 0.97 0.81 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.226 s]
Raw data (loadavg): 0.99 0.97 0.81 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.226 s]
Raw data (loadavg): 0.99 0.97 0.81 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.226 s]
Raw data (loadavg): 0.99 0.97 0.81 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.226 s]
Raw data (loadavg): 0.99 0.97 0.82 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.226 s]
Raw data (loadavg): 0.99 0.97 0.82 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.226 s]
Raw data (loadavg): 0.99 0.97 0.82 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.226 s]
Raw data (loadavg): 0.99 0.97 0.82 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.226 s]
Raw data (loadavg): 0.99 0.97 0.82 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.226 s]
Raw data (loadavg): 0.99 0.97 0.82 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.227 s]
Raw data (loadavg): 0.99 0.97 0.82 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.226 s]
Raw data (loadavg): 0.99 0.97 0.82 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.226 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.227 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.227 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.228 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.228 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.227 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.227 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.228 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.229 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.228 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.228 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.227 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.227 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.228 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.229 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.228 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.229 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.23 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.231 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.231 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.231 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.231 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.231 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.231 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.232 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.232 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.232 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.232 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.233 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.232 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.232 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.233 s]
Raw data (loadavg): 0.99 0.97 0.86 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.232 s]
Raw data (loadavg): 0.99 0.97 0.86 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.233 s]
Raw data (loadavg): 0.99 0.97 0.86 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.232 s]
Raw data (loadavg): 0.99 0.97 0.86 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.232 s]
Raw data (loadavg): 0.99 0.97 0.86 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.233 s]
Raw data (loadavg): 0.99 0.97 0.86 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.23 s]
Raw data (loadavg): 0.99 0.97 0.86 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.23 s]
Raw data (loadavg): 0.99 0.97 0.86 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.23 s]
Raw data (loadavg): 0.99 0.97 0.86 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.23 s]
Raw data (loadavg): 0.99 0.97 0.86 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.23 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.23 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.23 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.23 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.23 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.23 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.23 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.23 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.23 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.23 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.23 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.23 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.24 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.24 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.24 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.24 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.24 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.24 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.24 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.71 s]
Raw data (loadavg): 0.99 0.97 0.88 1/53 27022
Raw data (stat): 27018 (minisat+_script) S 27017 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853321911 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.71
CPU time (s): 1229.85
CPU user time (s): 1229.45
CPU system time (s): 0.404938
CPU usage (%): 100.012
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####