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-ii32d2.opb
MD5SUM	a483fc3761bb4050329265bf3a3a7ca5
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	372
Optimality of the best value was proved	NO
Number of terms in the objective function	808
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	808
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	808
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.04284
Number of variables	808
Total number of constraints	5557
Number of constraints which are clauses	5557
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	32
Trace number 30381

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc29 THE 2005-05-25 16:27:36 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=21738 boxname=wulflinc29 idbench=156 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  a483fc3761bb4050329265bf3a3a7ca5  /oldhome/oroussel/tmp/wulflinc29/normalized-ii32d2.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc29/normalized-ii32d2.opb
IDLAUNCH: 21738
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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.020
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:        488392 kB
Buffers:         34872 kB
Cached:         486184 kB
SwapCached:        572 kB
Active:          63448 kB
Inactive:       463148 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        488140 kB
SwapTotal:     2097892 kB
SwapFree:      2096728 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           5612 kB
Slab:            14060 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-25 16:48:06 (client local time) WITH STATUS 152 IN 1229.85 SECONDS
stats: 21738 7 1229.85 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 5557 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 |    5557    18748 |    1852       0        0     nan |  0.000 % |
c |       100 |    5557    18748 |    2037     100     8211    82.1 |  0.006 % |
c |       252 |    5557    18748 |    2240     252    19966    79.2 |  0.000 % |
c |       477 |    5557    18748 |    2465     477    34035    71.4 |  0.000 % |
c |       816 |    5557    18748 |    2711     816    61162    75.0 |  0.000 % |
c |      1322 |    5557    18748 |    2982    1322   101974    77.1 |  0.000 % |
c |      2082 |    5557    18748 |    3280    2082   175391    84.2 |  0.000 % |
c |      3222 |    5557    18748 |    3609    3222   287281    89.2 |  0.000 % |
c |      4930 |    5557    18748 |    3969    3034   259982    85.7 |  0.000 % |
c |      7492 |    5557    18748 |    4366    3524   289629    82.2 |  0.000 % |
c ==============================================================================
c [1mFound solution: 386[0m
c ---[   0]---> Sorter-cost:37286     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8400 |   50849   124642 |   16949    4432   356590    80.5 |  0.000 % |
c |      8500 |   50849   124642 |   18643    4532   364865    80.5 |  0.033 % |
c |      8650 |   50849   124642 |   20508    4682   378388    80.8 |  0.033 % |
c |      8875 |   50835   124614 |   22559    4906   393775    80.3 |  0.055 % |
c |      9214 |   50835   124614 |   24815    5245   423878    80.8 |  0.055 % |
c |      9720 |   50835   124614 |   27296    5751   464928    80.8 |  0.055 % |
c |     10479 |   50835   124614 |   30026    6510   536138    82.4 |  0.055 % |
c |     11619 |   50835   124614 |   33028    7650   644338    84.2 |  0.055 % |
c |     13328 |   50835   124614 |   36331    9359   803264    85.8 |  0.055 % |
c |     15892 |   50835   124614 |   39964   11923  1011917    84.9 |  0.055 % |
c |     19736 |   50819   124582 |   43961   15766  1313225    83.3 |  0.081 % |
c |     25502 |   50819   124582 |   48357   21532  1829113    84.9 |  0.081 % |
c |     34154 |   50496   123909 |   53193   30138  2562415    85.0 |  0.650 % |
c |     47129 |   50477   123870 |   58512   43112  3694785    85.7 |  0.683 % |
c |     66590 |   50370   123647 |   64363   19893  1410152    70.9 |  0.871 % |
c ==============================================================================
c [1mFound solution: 374[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     72696 |   49782   122492 |   16594   25929  1997415    77.0 |  0.871 % |
c |     72798 |   49745   122413 |   18253   13066   980835    75.1 |  2.403 % |
c |     72948 |   49745   122413 |   20078   13216   995146    75.3 |  2.403 % |
c |     73175 |   49745   122413 |   22086   13443  1023685    76.2 |  2.403 % |
c |     73514 |   49715   122349 |   24295   13781  1055470    76.6 |  2.455 % |
c |     74020 |   49715   122349 |   26724   14287  1097966    76.9 |  2.455 % |
c |     74780 |   49679   122273 |   29397   15046  1160728    77.1 |  2.520 % |
c |     75921 |   49640   122190 |   32337   16186  1244649    76.9 |  2.591 % |
c ==============================================================================
c [1mFound solution: 373[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     76756 |   49684   122335 |   16561   17021  1322203    77.7 |  2.591 % |
c |     76856 |   47021   116453 |   18217   17038  1322673    77.6 |  7.739 % |
c |     77006 |   46205   114637 |   20038   17161  1328197    77.4 |  9.357 % |
c |     77231 |   46205   114637 |   22042   17386  1343048    77.2 |  9.357 % |
c |     77569 |   46205   114637 |   24246   17724  1365837    77.1 |  9.357 % |
c |     78078 |   46151   114515 |   26671   18232  1404045    77.0 |  9.467 % |
c |     78840 |   46101   114405 |   29338   18993  1463530    77.1 |  9.564 % |
c |     79981 |   46043   114277 |   32272   20132  1550128    77.0 |  9.677 % |
c |     81689 |   46043   114277 |   35499   21840  1673169    76.6 |  9.677 % |
c |     84252 |   45935   114043 |   39049   24396  1851087    75.9 |  9.881 % |
c |     88099 |   45891   113943 |   42954   28242  2169099    76.8 |  9.972 % |
c |     93868 |   45833   113813 |   47250   34008  2666510    78.4 | 10.088 % |
c |    102517 |   45519   113123 |   51975   42638  3411087    80.0 | 10.697 % |
c ==============================================================================
c [1mFound solution: 372[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    115430 |   44752   111423 |   14917   55429  4585559    82.7 | 10.697 % |
c |    115531 |   44685   111278 |   16408   16626  1236706    74.4 | 12.317 % |
c |    115681 |   44643   111190 |   18049   16617  1236062    74.4 | 12.391 % |
c |    115906 |   44643   111190 |   19854   16842  1249766    74.2 | 12.391 % |
c |    116243 |   44643   111190 |   21839   17179  1266518    73.7 | 12.391 % |
c |    116749 |   44643   111190 |   24023   17685  1298014    73.4 | 12.391 % |
c |    117509 |   44586   111061 |   26426   18444  1346422    73.0 | 12.508 % |
c |    118648 |   44586   111061 |   29069   19583  1427861    72.9 | 12.508 % |
c |    120356 |   44586   111061 |   31975   21291  1567161    73.6 | 12.508 % |
c |    122918 |   44586   111061 |   35173   23853  1778453    74.6 | 12.508 % |
c |    126762 |   44586   111061 |   38690   27697  2063517    74.5 | 12.508 % |
c |    132528 |   44586   111061 |   42559   33463  2536232    75.8 | 12.508 % |
c |    141177 |   44353   110536 |   46815   42106  3294557    78.2 | 12.980 % |
c |    154151 |   44113   110002 |   51497   20387  1050521    51.5 | 13.456 % |
c |    173612 |   43984   109719 |   56647   39845  2733175    68.6 | 13.705 % |
c |    202804 |   43797   109306 |   62312   25456  1873780    73.6 | 14.070 % |
c |    246599 |   43412   108459 |   68543   21309  2135859   100.2 | 14.818 % |
/oldhome/oroussel/solvers/minisat+_script: line 9:  2646 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.86 0.94 0.97 2/54 2642
Raw data (stat): 2642 (runsolver) R 2641 20001 20000 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 840311215 1052672 99 4294967295 134512640 135381576 3221224496 3221219704 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.88 0.94 0.97 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.90 0.94 0.97 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0022 s]
Raw data (loadavg): 0.92 0.94 0.97 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0026 s]
Raw data (loadavg): 0.93 0.94 0.97 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0038 s]
Raw data (loadavg): 0.94 0.94 0.97 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0036 s]
Raw data (loadavg): 0.95 0.95 0.97 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0039 s]
Raw data (loadavg): 0.95 0.95 0.97 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0052 s]
Raw data (loadavg): 0.96 0.95 0.97 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0059 s]
Raw data (loadavg): 0.97 0.95 0.97 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.006 s]
Raw data (loadavg): 0.97 0.95 0.97 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.007 s]
Raw data (loadavg): 0.98 0.95 0.97 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.007 s]
Raw data (loadavg): 0.98 0.95 0.97 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.008 s]
Raw data (loadavg): 0.98 0.95 0.97 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.009 s]
Raw data (loadavg): 0.98 0.95 0.97 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.01 s]
Raw data (loadavg): 0.99 0.95 0.97 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.009 s]
Raw data (loadavg): 0.99 0.95 0.97 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.01 s]
Raw data (loadavg): 0.99 0.96 0.97 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.011 s]
Raw data (loadavg): 0.99 0.96 0.97 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.012 s]
Raw data (loadavg): 0.99 0.96 0.97 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.013 s]
Raw data (loadavg): 0.99 0.96 0.97 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.012 s]
Raw data (loadavg): 0.99 0.96 0.97 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.013 s]
Raw data (loadavg): 0.99 0.96 0.97 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.013 s]
Raw data (loadavg): 0.99 0.96 0.97 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.013 s]
Raw data (loadavg): 0.99 0.96 0.97 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.014 s]
Raw data (loadavg): 0.99 0.96 0.97 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.014 s]
Raw data (loadavg): 0.99 0.96 0.97 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.015 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.015 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.016 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.016 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.017 s]
Raw data (loadavg): 1.07 0.99 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.018 s]
Raw data (loadavg): 1.06 0.99 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.017 s]
Raw data (loadavg): 1.05 0.99 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.017 s]
Raw data (loadavg): 1.04 0.99 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.018 s]
Raw data (loadavg): 1.04 0.99 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.019 s]
Raw data (loadavg): 1.03 0.99 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.02 s]
Raw data (loadavg): 1.03 0.99 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.02 s]
Raw data (loadavg): 1.02 0.99 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.02 s]
Raw data (loadavg): 1.02 0.99 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.02 s]
Raw data (loadavg): 1.09 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.021 s]
Raw data (loadavg): 1.08 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.022 s]
Raw data (loadavg): 1.07 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.022 s]
Raw data (loadavg): 1.06 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.022 s]
Raw data (loadavg): 1.05 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.022 s]
Raw data (loadavg): 1.04 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.023 s]
Raw data (loadavg): 1.03 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.024 s]
Raw data (loadavg): 1.03 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.024 s]
Raw data (loadavg): 1.02 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.024 s]
Raw data (loadavg): 1.02 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.024 s]
Raw data (loadavg): 1.02 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.024 s]
Raw data (loadavg): 1.01 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.025 s]
Raw data (loadavg): 1.01 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.026 s]
Raw data (loadavg): 1.01 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.026 s]
Raw data (loadavg): 1.01 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.027 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.028 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.028 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.028 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.029 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.03 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.031 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.032 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.032 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.032 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.032 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.033 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.034 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.033 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.034 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.034 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.035 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.035 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.035 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.036 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.035 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.037 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.037 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.037 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.038 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.038 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.038 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.038 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.038 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.039 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.039 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.04 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.04 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.04 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.041 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.041 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.04 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.041 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.041 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.041 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.04 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.04 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.04 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.04 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.04 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.04 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.04 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.04 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.04 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.04 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.04 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.04 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.04 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.04 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.04 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.04 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.00 1.00 0.98 1/53 2646
Raw data (stat): 2642 (minisat+_script) S 2641 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840311215 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.85
CPU user time (s): 1229.25
CPU system time (s): 0.606907
CPU usage (%): 100.006
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####