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-ii16b1.opb
MD5SUM	dd9b4ae34921e1731f1a12dcd9d29b23
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1528
Optimality of the best value was proved	NO
Number of terms in the objective function	3456
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	3456
Number of bits of the sum of numbers in the objective function	12
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	3456
Number of bits of the biggest sum of numbers	12
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.09
Number of variables	3456
Total number of constraints	26520
Number of constraints which are clauses	26520
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	16
Trace number 31532

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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:        634144 kB
Buffers:         39092 kB
Cached:         332960 kB
SwapCached:        588 kB
Active:          66892 kB
Inactive:       310532 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        633892 kB
SwapTotal:     2097892 kB
SwapFree:      2096632 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5668 kB
Slab:            17516 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-27 05:02:06 (client local time) WITH STATUS 152 IN 1229.88 SECONDS
stats: 22892 7 1229.88 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 26520 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 |   26520    67136 |    8840       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 1663[0m
c ---[   0]---> Sorter-cost:233218     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        90 |  320186   753282 |  106728      90     2917    32.4 |  0.000 % |
c |       190 |  320186   753282 |  117400     190     8467    44.6 |  0.001 % |
c |       340 |  320168   753246 |  129140     339    14755    43.5 |  0.005 % |
c |       566 |  320168   753246 |  142054     565    24084    42.6 |  0.005 % |
c |       903 |  319742   752350 |  156260     869    31937    36.8 |  0.124 % |
c |      1409 |  319742   752350 |  171886    1375    42446    30.9 |  0.124 % |
c |      2169 |  319742   752350 |  189075    2135    56472    26.5 |  0.124 % |
c |      3308 |  319742   752350 |  207982    3274    79862    24.4 |  0.124 % |
c |      5018 |  319532   751910 |  228780    4978   162940    32.7 |  0.181 % |
c |      7580 |  319072   750924 |  251659    7228   241448    33.4 |  0.313 % |
c ==============================================================================
c [1mFound solution: 1657[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9280 |  318688   750266 |  106229    8918   301951    33.9 |  0.313 % |
c |      9380 |  317572   747856 |  116851    8991   303411    33.7 |  0.785 % |
c |      9531 |  317572   747856 |  128537    9142   308430    33.7 |  0.785 % |
c |      9757 |  317572   747856 |  141390    9368   317137    33.9 |  0.785 % |
c |     10094 |  317572   747856 |  155529    9705   330372    34.0 |  0.785 % |
c |     10600 |  317311   747297 |  171082   10203   348885    34.2 |  0.860 % |
c |     11361 |  317311   747297 |  188191   10964   393881    35.9 |  0.860 % |
c |     12505 |  312064   735817 |  207010   11993   438187    36.5 |  2.421 % |
c ==============================================================================
c [1mFound solution: 1629[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13450 |  312390   736834 |  104130   12938   472872    36.5 |  2.421 % |
c |     13550 |  312390   736834 |  114543   13038   475304    36.5 |  2.467 % |
c |     13701 |  312390   736834 |  125997   13189   482299    36.6 |  2.467 % |
c |     13926 |  312390   736834 |  138597   13414   500311    37.3 |  2.467 % |
c |     14263 |  312199   736427 |  152456   13748   510688    37.1 |  2.521 % |
c |     14770 |  312199   736427 |  167702   14255   521838    36.6 |  2.521 % |
c |     15529 |  312148   736316 |  184472   15010   535637    35.7 |  2.536 % |
c |     16668 |  312148   736316 |  202919   16149   566573    35.1 |  2.536 % |
c |     18376 |  311226   734247 |  223211   17551   605280    34.5 |  2.817 % |
c |     20939 |  311127   734030 |  245533   20106   785493    39.1 |  2.846 % |
c |     24783 |  311127   734030 |  270086   23950  2365323    98.8 |  2.846 % |
c |     30550 |  306429   723606 |  297095   29274  2741918    93.7 |  4.286 % |
c |     39199 |  305644   721875 |  326804   37908  3449384    91.0 |  4.523 % |
c ==============================================================================
c [1mFound solution: 1626[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     45826 |  305660   721920 |  101886   44428  5060295   113.9 |  4.523 % |
c |     45927 |  305660   721920 |  112074   44529  5068527   113.8 |  4.531 % |
c |     46083 |  305523   721625 |  123282   44683  5070897   113.5 |  4.571 % |
c |     46308 |  305523   721625 |  135610   44908  5073782   113.0 |  4.571 % |
c |     46645 |  305523   721625 |  149171   45245  5084729   112.4 |  4.571 % |
c |     47151 |  305459   721485 |  164088   45750  5102608   111.5 |  4.590 % |
c |     47910 |  305203   720911 |  180497   46503  5146294   110.7 |  4.670 % |
c |     49049 |  305054   720578 |  198546   47635  5193146   109.0 |  4.717 % |
c |     50758 |  304873   720175 |  218401   49336  5272433   106.9 |  4.772 % |
c |     53320 |  304648   719666 |  240241   51892  5329507   102.7 |  4.843 % |
c |     57164 |  304140   718544 |  264266   55276  5743464   103.9 |  4.998 % |
c ==============================================================================
c [1mFound solution: 1594[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     62049 |  304485   719549 |  101495   60070  6159044   102.5 |  4.998 % |
c |     62151 |  304485   719549 |  111644   60172  6162200   102.4 |  5.056 % |
c |     62301 |  304485   719549 |  122808   60322  6179331   102.4 |  5.056 % |
c |     62527 |  304334   719212 |  135089   60541  6190719   102.3 |  5.130 % |
c |     62865 |  304245   719013 |  148598   60879  6212145   102.0 |  5.130 % |
c |     63371 |  304245   719013 |  163458   61385  6224136   101.4 |  5.130 % |
c |     64130 |  304245   719013 |  179804   62144  6301640   101.4 |  5.130 % |
c |     65269 |  304067   718623 |  197785   63275  6424358   101.5 |  5.183 % |
c |     66977 |  303731   717887 |  217563   64942  6492420   100.0 |  5.284 % |
c |     69540 |  303569   717511 |  239319   67501  6864271   101.7 |  5.338 % |
c ==============================================================================
c [1mFound solution: 1518[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     72694 |  304258   719388 |  101419   70475  6896701    97.9 |  5.338 % |
c |     72794 |  304258   719388 |  111560   70575  6899948    97.8 |  5.457 % |
c |     72944 |  304258   719388 |  122716   70725  6905746    97.6 |  5.457 % |
c |     73169 |  304258   719388 |  134988   70950  6915583    97.5 |  5.457 % |
c |     73506 |  304258   719388 |  148487   71287  6992359    98.1 |  5.457 % |
c |     74013 |  304190   719234 |  163336   71793  7010176    97.6 |  5.479 % |
c |     74772 |  304131   719101 |  179669   72545  7028696    96.9 |  5.497 % |
c |     75911 |  303859   718503 |  197636   73680  7099034    96.3 |  5.579 % |
c |     77621 |  303566   717850 |  217400   75384  7320446    97.1 |  5.669 % |
c |     80185 |  303445   717575 |  239140   77510  7507397    96.9 |  5.708 % |
c |     84030 |  303367   717407 |  263054   81354  7784138    95.7 |  5.730 % |
c ==============================================================================
c [1mFound solution: 1457[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     84293 |  303975   719064 |  101325   81617  7797398    95.5 |  5.730 % |
c |     84393 |  303975   719064 |  111457   81717  7806615    95.5 |  5.809 % |
c |     84543 |  303975   719064 |  122603   81867  7841702    95.8 |  5.809 % |
c |     84768 |  303975   719064 |  134863   82092  7848758    95.6 |  5.809 % |
c |     85105 |  303975   719064 |  148349   82429  7852361    95.3 |  5.809 % |
c |     85611 |  303975   719064 |  163184   82935  7883531    95.1 |  5.809 % |
c |     86371 |  303767   718600 |  179503   83683  7985004    95.4 |  5.873 % |
c |     87510 |  302981   716842 |  197453   84759  8042610    94.9 |  6.116 % |
c |     89218 |  302981   716842 |  217199   86467  8120104    93.9 |  6.116 % |
c |     91780 |  302753   716348 |  238919   89023  8456162    95.0 |  6.182 % |
c |     95624 |  302146   714977 |  262810   92847  8738710    94.1 |  6.373 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 11969 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 11965
Raw data (stat): 11965 (runsolver) R 11964 24172 24171 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 853347075 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.0003 s]
Raw data (loadavg): 0.93 0.95 0.70 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.0014 s]
Raw data (loadavg): 0.94 0.96 0.70 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.002 s]
Raw data (loadavg): 0.95 0.96 0.71 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.0019 s]
Raw data (loadavg): 0.96 0.96 0.71 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.0028 s]
Raw data (loadavg): 0.96 0.96 0.71 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.0027 s]
Raw data (loadavg): 0.97 0.96 0.72 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.0036 s]
Raw data (loadavg): 0.97 0.96 0.72 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.0039 s]
Raw data (loadavg): 0.98 0.96 0.72 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.0035 s]
Raw data (loadavg): 0.98 0.96 0.72 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.003 s]
Raw data (loadavg): 0.98 0.96 0.73 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.004 s]
Raw data (loadavg): 0.98 0.96 0.73 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.004 s]
Raw data (loadavg): 0.99 0.97 0.73 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.004 s]
Raw data (loadavg): 0.99 0.97 0.73 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.004 s]
Raw data (loadavg): 0.99 0.97 0.74 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.005 s]
Raw data (loadavg): 0.99 0.97 0.74 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.005 s]
Raw data (loadavg): 0.99 0.97 0.74 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.005 s]
Raw data (loadavg): 0.99 0.97 0.74 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.005 s]
Raw data (loadavg): 0.99 0.97 0.74 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.005 s]
Raw data (loadavg): 0.99 0.97 0.75 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.006 s]
Raw data (loadavg): 0.99 0.97 0.75 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.006 s]
Raw data (loadavg): 0.99 0.97 0.75 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.007 s]
Raw data (loadavg): 0.99 0.97 0.75 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.007 s]
Raw data (loadavg): 0.99 0.97 0.75 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.006 s]
Raw data (loadavg): 0.99 0.97 0.76 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.006 s]
Raw data (loadavg): 0.99 0.97 0.76 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.007 s]
Raw data (loadavg): 0.99 0.97 0.76 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.007 s]
Raw data (loadavg): 0.99 0.97 0.76 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.007 s]
Raw data (loadavg): 0.99 0.97 0.76 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.008 s]
Raw data (loadavg): 0.99 0.97 0.77 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.008 s]
Raw data (loadavg): 0.99 0.97 0.77 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.008 s]
Raw data (loadavg): 0.99 0.97 0.77 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.009 s]
Raw data (loadavg): 0.99 0.97 0.77 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.009 s]
Raw data (loadavg): 0.99 0.97 0.77 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.009 s]
Raw data (loadavg): 0.99 0.97 0.77 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.009 s]
Raw data (loadavg): 0.99 0.97 0.78 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.01 s]
Raw data (loadavg): 0.99 0.97 0.78 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.011 s]
Raw data (loadavg): 0.99 0.97 0.78 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.011 s]
Raw data (loadavg): 0.99 0.97 0.78 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.011 s]
Raw data (loadavg): 0.99 0.97 0.78 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.012 s]
Raw data (loadavg): 0.99 0.97 0.79 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.012 s]
Raw data (loadavg): 0.99 0.97 0.79 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.013 s]
Raw data (loadavg): 0.99 0.97 0.79 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.014 s]
Raw data (loadavg): 0.99 0.97 0.79 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.014 s]
Raw data (loadavg): 0.99 0.97 0.79 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.015 s]
Raw data (loadavg): 0.99 0.97 0.80 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.016 s]
Raw data (loadavg): 0.99 0.97 0.80 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.017 s]
Raw data (loadavg): 0.99 0.97 0.80 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.018 s]
Raw data (loadavg): 0.99 0.97 0.80 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.018 s]
Raw data (loadavg): 0.99 0.97 0.80 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.019 s]
Raw data (loadavg): 0.99 0.97 0.81 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.02 s]
Raw data (loadavg): 0.99 0.97 0.81 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.02 s]
Raw data (loadavg): 0.99 0.97 0.81 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.024 s]
Raw data (loadavg): 0.99 0.97 0.81 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.024 s]
Raw data (loadavg): 0.99 0.97 0.81 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.024 s]
Raw data (loadavg): 0.99 0.97 0.82 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.025 s]
Raw data (loadavg): 0.99 0.97 0.82 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.025 s]
Raw data (loadavg): 0.99 0.97 0.82 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.025 s]
Raw data (loadavg): 0.99 0.97 0.82 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.026 s]
Raw data (loadavg): 0.99 0.97 0.82 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.026 s]
Raw data (loadavg): 0.99 0.97 0.82 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.026 s]
Raw data (loadavg): 0.99 0.97 0.82 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.028 s]
Raw data (loadavg): 0.99 0.97 0.82 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.028 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.028 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.029 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.028 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.029 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.03 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.03 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.031 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.032 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.032 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.032 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.033 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.033 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.033 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.034 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.035 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.035 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.035 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.036 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.037 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.037 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.037 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.037 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.037 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.038 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.038 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.038 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.039 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.039 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.041 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.041 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.041 s]
Raw data (loadavg): 0.99 0.97 0.86 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.041 s]
Raw data (loadavg): 0.99 0.97 0.86 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.041 s]
Raw data (loadavg): 0.99 0.97 0.86 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.042 s]
Raw data (loadavg): 0.99 0.97 0.86 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.043 s]
Raw data (loadavg): 0.99 0.97 0.86 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.042 s]
Raw data (loadavg): 0.99 0.97 0.86 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.04 s]
Raw data (loadavg): 0.99 0.97 0.86 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.04 s]
Raw data (loadavg): 0.99 0.97 0.86 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.04 s]
Raw data (loadavg): 0.99 0.97 0.86 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.04 s]
Raw data (loadavg): 0.99 0.97 0.86 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.04 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.04 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.04 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.05 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.05 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.05 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.05 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 11969
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.05 s]
Raw data (loadavg): 0.99 0.97 0.87 2/58 11972
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.05 s]
Raw data (loadavg): 1.23 1.02 0.89 2/59 12012
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.05 s]
Raw data (loadavg): 1.27 1.04 0.90 2/55 12022
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.15 s]
Raw data (loadavg): 1.22 1.03 0.90 2/55 12022
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.15 s]
Raw data (loadavg): 1.19 1.03 0.90 2/55 12022
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.15 s]
Raw data (loadavg): 1.16 1.03 0.90 2/55 12022
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.15 s]
Raw data (loadavg): 1.13 1.03 0.90 2/55 12022
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.15 s]
Raw data (loadavg): 1.11 1.03 0.90 2/55 12022
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.15 s]
Raw data (loadavg): 1.10 1.03 0.90 2/55 12022
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.15 s]
Raw data (loadavg): 1.08 1.03 0.90 2/55 12024
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.15 s]
Raw data (loadavg): 1.07 1.02 0.90 2/55 12024
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.15 s]
Raw data (loadavg): 1.06 1.02 0.90 2/55 12024
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.78 s]
Raw data (loadavg): 1.05 1.02 0.91 1/53 12024
Raw data (stat): 11965 (minisat+_script) S 11964 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853347075 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.78
CPU time (s): 1229.88
CPU user time (s): 1229.01
CPU system time (s): 0.870867
CPU usage (%): 100.008
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####