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-ii8a2.opb
MD5SUM	6005a01d3f2ae55b0ca9c19f876c5827
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	139
Optimality of the best value was proved	NO
Number of terms in the objective function	360
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	360
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	360
Number of bits of the biggest sum of numbers	9
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02584
Number of variables	360
Total number of constraints	980
Number of constraints which are clauses	980
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	8
Trace number 31573

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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:        887288 kB
Buffers:         33328 kB
Cached:          89332 kB
SwapCached:        692 kB
Active:          62984 kB
Inactive:        62020 kB
HighTotal:      131008 kB
HighFree:        38780 kB
LowTotal:       903652 kB
LowFree:        848508 kB
SwapTotal:     2097136 kB
SwapFree:      2095440 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5780 kB
Slab:            16576 kB
Committed_AS:    92716 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-27 05:14:33 (client local time) WITH STATUS 152 IN 1229.84 SECONDS
stats: 22918 7 1229.84 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 980 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 |     980     2412 |     326       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 150[0m
c ---[   0]---> Sorter-cost:13276     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         3 |   16839    39488 |    5613       3       20     6.7 |  0.000 % |
c |       103 |   16491    38744 |    6174      90     1250    13.9 |  1.915 % |
c |       254 |   16341    38418 |    6791     234     5528    23.6 |  2.729 % |
c |       479 |   16038    37759 |    7470     450    11949    26.6 |  4.320 % |
c |       817 |   15269    36066 |    8217     770    24110    31.3 |  8.575 % |
c |      1323 |   15221    35960 |    9039    1275    41757    32.8 |  8.844 % |
c |      2082 |   15221    35960 |    9943    2034    93705    46.1 |  8.844 % |
c ==============================================================================
c [1mFound solution: 148[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2350 |   15217    35960 |    5072    2302   101593    44.1 |  8.844 % |
c |      2450 |   15217    35960 |    5579    2402   105288    43.8 |  9.084 % |
c |      2600 |   15217    35960 |    6137    2552   107574    42.2 |  9.084 % |
c ==============================================================================
c [1mFound solution: 142[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2813 |   15257    36064 |    5085    2763   111341    40.3 |  9.084 % |
c |      2915 |   15257    36064 |    5593    2865   112507    39.3 |  9.266 % |
c |      3065 |   15257    36064 |    6152    3015   115583    38.3 |  9.266 % |
c |      3290 |   15213    35964 |    6768    3239   129038    39.8 |  9.524 % |
c |      3631 |   15119    35756 |    7444    3575   143929    40.3 | 10.048 % |
c |      4137 |   15119    35756 |    8189    4081   159776    39.2 | 10.048 % |
c |      4896 |   15119    35756 |    9008    4840   198324    41.0 | 10.048 % |
c |      6037 |   15119    35756 |    9909    5981   259812    43.4 | 10.048 % |
c |      7746 |   15119    35756 |   10900    7690   319662    41.6 | 10.048 % |
c |     10309 |   15020    35539 |   11990   10251   449968    43.9 | 10.590 % |
c |     14154 |   15020    35539 |   13189    7241   321460    44.4 | 10.590 % |
c |     19920 |   14964    35421 |   14508   13006   623303    47.9 | 10.875 % |
c ==============================================================================
c [1mFound solution: 141[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27771 |   14986    35486 |    4995   11967   651063    54.4 | 10.875 % |
c |     27872 |   14986    35486 |    5494    6085   308059    50.6 | 10.927 % |
c |     28024 |   14931    35351 |    6043    6229   312203    50.1 | 11.294 % |
c |     28250 |   14825    35119 |    6648    6439   321374    49.9 | 11.853 % |
c |     28588 |   14825    35119 |    7313    6777   330987    48.8 | 11.853 % |
c |     29095 |   14825    35119 |    8044    7284   349008    47.9 | 11.853 % |
c |     29854 |   14825    35119 |    8848    8043   376752    46.8 | 11.853 % |
c |     30994 |   14825    35119 |    9733    9183   417078    45.4 | 11.853 % |
c |     32702 |   14791    35041 |   10707   10887   478885    44.0 | 12.055 % |
c |     35264 |   14791    35041 |   11777    7145   253382    35.5 | 12.055 % |
c |     39109 |   14791    35041 |   12955   10990   474654    43.2 | 12.055 % |
c |     44877 |   14791    35041 |   14251    9411   454007    48.2 | 12.055 % |
c |     53527 |   14791    35041 |   15676    9296   440843    47.4 | 12.055 % |
c |     66501 |   14791    35041 |   17244   12660   591539    46.7 | 12.055 % |
c |     85962 |   14752    34954 |   18968   12206   509154    41.7 | 12.275 % |
c |    115155 |   14752    34954 |   20865   19570   994956    50.8 | 12.275 % |
c |    158944 |   14752    34954 |   22951   15966   812506    50.9 | 12.275 % |
c |    224628 |   14752    34954 |   25247   16504   780085    47.3 | 12.275 % |
c ==============================================================================
c [1mFound solution: 139[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    273203 |   14737    34933 |    4912   22747  1178259    51.8 | 12.275 % |
c |    273303 |   14737    34933 |    5403    5787   220361    38.1 | 12.486 % |
c |    273453 |   14737    34933 |    5943    5937   224417    37.8 | 12.486 % |
c |    273678 |   14673    34785 |    6537    6143   232659    37.9 | 12.871 % |
c |    274016 |   14673    34785 |    7191    6481   247623    38.2 | 12.871 % |
c |    274524 |   14673    34785 |    7910    6989   269613    38.6 | 12.871 % |
c |    275284 |   14673    34785 |    8701    7749   306748    39.6 | 12.871 % |
c |    276423 |   14673    34785 |    9572    8888   356210    40.1 | 12.871 % |
c |    278132 |   14636    34702 |   10529   10596   451584    42.6 | 13.082 % |
c |    280694 |   14636    34702 |   11582    6651   294921    44.3 | 13.082 % |
c |    284538 |   14636    34702 |   12740   10495   503132    47.9 | 13.082 % |
c |    290305 |   14636    34702 |   14014    8572   373798    43.6 | 13.082 % |
c |    298954 |   14636    34702 |   15415    8671   427916    49.4 | 13.082 % |
c |    311928 |   14567    34547 |   16957   12461   746270    59.9 | 13.476 % |
c |    331389 |   14567    34547 |   18653   12412   552554    44.5 | 13.476 % |
c |    360584 |   14567    34547 |   20518   20300  1026218    50.6 | 13.476 % |
c |    404373 |   14567    34547 |   22570   17926   952975    53.2 | 13.476 % |
c |    470057 |   14567    34547 |   24827   21071  1096971    52.1 | 13.476 % |
c |    568587 |   14539    34481 |   27310   23204  1046969    45.1 | 13.650 % |
/oldhome/oroussel/solvers/minisat+_script: line 9:  1076 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.85 0.92 0.81 2/55 1072
Raw data (stat): 1072 (runsolver) R 1071 8378 8377 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 738358286 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0015 s]
Raw data (loadavg): 0.87 0.92 0.81 2/56 1076
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0018 s]
Raw data (loadavg): 0.89 0.92 0.82 2/56 1076
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0016 s]
Raw data (loadavg): 0.91 0.92 0.82 2/56 1076
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0015 s]
Raw data (loadavg): 0.92 0.92 0.82 2/56 1076
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0023 s]
Raw data (loadavg): 0.93 0.93 0.82 2/56 1076
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0032 s]
Raw data (loadavg): 0.94 0.93 0.82 2/56 1076
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0045 s]
Raw data (loadavg): 0.95 0.93 0.82 2/56 1076
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0048 s]
Raw data (loadavg): 0.96 0.93 0.82 2/56 1076
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0057 s]
Raw data (loadavg): 0.96 0.93 0.82 2/56 1076
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.005 s]
Raw data (loadavg): 0.97 0.94 0.82 2/56 1076
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.006 s]
Raw data (loadavg): 0.97 0.94 0.83 2/56 1076
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.007 s]
Raw data (loadavg): 0.98 0.94 0.83 2/56 1076
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.007 s]
Raw data (loadavg): 0.98 0.94 0.83 2/56 1076
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.008 s]
Raw data (loadavg): 0.98 0.94 0.83 2/56 1076
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.009 s]
Raw data (loadavg): 0.98 0.94 0.83 2/56 1076
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.009 s]
Raw data (loadavg): 0.99 0.94 0.83 2/56 1076
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.009 s]
Raw data (loadavg): 0.99 0.95 0.83 2/56 1076
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.009 s]
Raw data (loadavg): 0.99 0.95 0.83 2/56 1076
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.01 s]
Raw data (loadavg): 0.99 0.95 0.83 2/56 1076
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.011 s]
Raw data (loadavg): 0.99 0.95 0.83 2/56 1076
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.011 s]
Raw data (loadavg): 0.99 0.95 0.84 2/56 1076
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.012 s]
Raw data (loadavg): 0.99 0.95 0.84 2/56 1076
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.012 s]
Raw data (loadavg): 0.99 0.95 0.84 2/56 1076
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.013 s]
Raw data (loadavg): 0.99 0.95 0.84 2/56 1076
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.013 s]
Raw data (loadavg): 0.99 0.95 0.84 2/56 1076
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.015 s]
Raw data (loadavg): 0.99 0.95 0.84 2/56 1076
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.014 s]
Raw data (loadavg): 0.99 0.96 0.84 2/56 1076
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.014 s]
Raw data (loadavg): 0.99 0.96 0.84 2/56 1076
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.015 s]
Raw data (loadavg): 0.99 0.96 0.84 2/56 1076
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.015 s]
Raw data (loadavg): 0.99 0.96 0.84 2/56 1076
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.016 s]
Raw data (loadavg): 0.99 0.96 0.85 2/56 1076
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.017 s]
Raw data (loadavg): 0.99 0.96 0.85 2/56 1076
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.016 s]
Raw data (loadavg): 0.99 0.96 0.85 2/56 1076
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.017 s]
Raw data (loadavg): 0.99 0.96 0.85 2/56 1076
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.017 s]
Raw data (loadavg): 0.99 0.96 0.85 2/56 1076
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.018 s]
Raw data (loadavg): 0.99 0.96 0.85 2/56 1076
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.205 s]
Raw data (loadavg): 0.99 0.97 0.85 2/56 1129
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.204 s]
Raw data (loadavg): 0.99 0.97 0.85 2/56 1129
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.204 s]
Raw data (loadavg): 0.99 0.97 0.85 2/56 1129
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.459 s]
Raw data (loadavg): 0.99 0.97 0.85 2/56 1129
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.46 s]
Raw data (loadavg): 0.99 0.97 0.85 2/56 1129
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.459 s]
Raw data (loadavg): 0.99 0.97 0.86 2/56 1131
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.46 s]
Raw data (loadavg): 0.99 0.97 0.86 2/56 1133
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.46 s]
Raw data (loadavg): 0.99 0.97 0.86 2/56 1133
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.46 s]
Raw data (loadavg): 0.99 0.97 0.86 2/56 1133
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.461 s]
Raw data (loadavg): 0.99 0.97 0.86 2/56 1133
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.461 s]
Raw data (loadavg): 0.99 0.97 0.86 2/56 1133
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.461 s]
Raw data (loadavg): 0.99 0.97 0.86 2/56 1133
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.461 s]
Raw data (loadavg): 0.99 0.97 0.86 2/56 1133
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.462 s]
Raw data (loadavg): 0.99 0.97 0.86 2/56 1133
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.463 s]
Raw data (loadavg): 0.99 0.97 0.86 2/56 1133
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.462 s]
Raw data (loadavg): 0.99 0.97 0.87 2/56 1133
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.462 s]
Raw data (loadavg): 0.99 0.97 0.87 2/56 1133
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.463 s]
Raw data (loadavg): 0.99 0.97 0.87 2/56 1133
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.463 s]
Raw data (loadavg): 0.99 0.97 0.87 2/56 1133
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.464 s]
Raw data (loadavg): 0.99 0.97 0.87 2/56 1133
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.465 s]
Raw data (loadavg): 0.99 0.97 0.87 2/56 1133
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.464 s]
Raw data (loadavg): 0.99 0.97 0.87 2/56 1133
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.464 s]
Raw data (loadavg): 0.99 0.97 0.87 2/56 1133
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.464 s]
Raw data (loadavg): 0.99 0.97 0.87 2/56 1133
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.465 s]
Raw data (loadavg): 0.99 0.97 0.87 2/56 1133
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.465 s]
Raw data (loadavg): 0.99 0.97 0.88 2/56 1133
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.464 s]
Raw data (loadavg): 0.99 0.97 0.88 2/56 1133
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.465 s]
Raw data (loadavg): 0.99 0.97 0.88 2/56 1133
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.465 s]
Raw data (loadavg): 0.99 0.97 0.88 2/56 1133
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.466 s]
Raw data (loadavg): 0.99 0.97 0.88 2/56 1133
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.466 s]
Raw data (loadavg): 0.99 0.97 0.88 2/56 1133
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.466 s]
Raw data (loadavg): 0.99 0.97 0.88 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.465 s]
Raw data (loadavg): 0.99 0.97 0.88 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.465 s]
Raw data (loadavg): 0.99 0.97 0.88 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.466 s]
Raw data (loadavg): 0.99 0.97 0.88 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.466 s]
Raw data (loadavg): 0.99 0.97 0.89 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.466 s]
Raw data (loadavg): 0.99 0.97 0.89 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.466 s]
Raw data (loadavg): 0.99 0.97 0.89 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.466 s]
Raw data (loadavg): 0.99 0.97 0.89 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.467 s]
Raw data (loadavg): 0.99 0.97 0.89 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.467 s]
Raw data (loadavg): 0.99 0.97 0.89 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.466 s]
Raw data (loadavg): 0.99 0.97 0.89 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.467 s]
Raw data (loadavg): 0.99 0.97 0.89 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.466 s]
Raw data (loadavg): 0.99 0.97 0.89 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.467 s]
Raw data (loadavg): 0.99 0.97 0.89 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.468 s]
Raw data (loadavg): 0.99 0.97 0.89 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.467 s]
Raw data (loadavg): 0.99 0.97 0.90 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.467 s]
Raw data (loadavg): 0.99 0.97 0.90 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.467 s]
Raw data (loadavg): 0.99 0.97 0.90 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.468 s]
Raw data (loadavg): 0.99 0.97 0.90 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.468 s]
Raw data (loadavg): 0.99 0.97 0.90 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.467 s]
Raw data (loadavg): 0.99 0.97 0.90 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.468 s]
Raw data (loadavg): 0.99 0.97 0.90 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.468 s]
Raw data (loadavg): 0.99 0.97 0.90 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.469 s]
Raw data (loadavg): 0.99 0.97 0.90 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.47 s]
Raw data (loadavg): 0.99 0.97 0.90 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.47 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.469 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.469 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.47 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.47 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.469 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.47 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.47 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.47 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.47 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.47 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.47 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.47 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.47 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.47 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.47 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.47 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.47 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.47 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.47 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.47 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.47 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.47 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.47 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.47 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.47 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.47 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.47 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.47 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.47 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.71 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 1135
Raw data (stat): 1072 (minisat+_script) S 1071 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738358286 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

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