PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/submitted/manquinho/logic-synthesis/normalized-prom2.pi.opb
MD5SUM	4a63080ba3e63c3b77e35782a700d569
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	330
Optimality of the best value was proved	NO
Number of terms in the objective function	2618
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	2618
Number of bits of the sum of numbers in the objective function	12
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	2618
Number of bits of the biggest sum of numbers	12
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.71974
Number of variables	2617
Total number of constraints	1988
Number of constraints which are clauses	1988
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	1
Maximum length of a constraint	30
Trace number 31493

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        878728 kB
Buffers:         34712 kB
Cached:          99456 kB
SwapCached:        608 kB
Active:          43192 kB
Inactive:        92984 kB
HighTotal:      131008 kB
HighFree:        46004 kB
LowTotal:       903652 kB
LowFree:        832724 kB
SwapTotal:     2097136 kB
SwapFree:      2095624 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5096 kB
Slab:            14248 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-27 04:56:14 (client local time) WITH STATUS 152 IN 1229.87 SECONDS
stats: 22825 7 1229.87 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1966 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ================
c   -- Clauses(.)/Splits(s): ........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    1944    15270 |     648       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 438[0m
c ---[   0]---> Sorter-cost:173028     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  213956   510135 |   71318       0        0     nan |  0.000 % |
c |       100 |  211045   503945 |   78449      39      229     5.9 |  1.180 % |
c |       250 |  208839   499197 |   86294     148     1116     7.5 |  2.066 % |
c |       475 |  207944   497228 |   94924     357     2725     7.6 |  2.443 % |
c |       812 |  207008   495163 |  104416     672     5926     8.8 |  2.834 % |
c |      1318 |  206464   493970 |  114858    1160    11078     9.6 |  3.060 % |
c |      2077 |  205360   491537 |  126344    1885    17253     9.2 |  3.523 % |
c |      3216 |  205144   491048 |  138978    3013    43555    14.5 |  3.618 % |
c |      4924 |  204057   488637 |  152876    4673    61214    13.1 |  4.077 % |
c |      7487 |  203673   487787 |  168164    7198    99047    13.8 |  4.239 % |
c |     11331 |  203303   486968 |  184980   11020   148770    13.5 |  4.393 % |
c |     17097 |  202804   485861 |  203478   16729   230769    13.8 |  4.603 % |
c |     25747 |  202434   485027 |  223826   25347   385130    15.2 |  4.762 % |
c |     38722 |  202393   484931 |  246209   38314   743803    19.4 |  4.781 % |
c ==============================================================================
c [1mFound solution: 384[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     55429 |  202712   485691 |   67570   55017  1170088    21.3 |  4.781 % |
c |     55530 |  202712   485691 |   74327   55118  1171692    21.3 |  4.802 % |
c |     55681 |  202712   485691 |   81759   55269  1173037    21.2 |  4.802 % |
c |     55906 |  202712   485691 |   89935   55494  1175747    21.2 |  4.802 % |
c |     56245 |  202712   485691 |   98929   55833  1182500    21.2 |  4.802 % |
c |     56751 |  202670   485601 |  108822   56335  1190446    21.1 |  4.819 % |
c |     57510 |  202670   485601 |  119704   57094  1206218    21.1 |  4.819 % |
c |     58650 |  202609   485454 |  131674   58227  1234697    21.2 |  4.849 % |
c |     60358 |  202609   485454 |  144842   59935  1266362    21.1 |  4.849 % |
c |     62921 |  202607   485450 |  159326   62485  1316403    21.1 |  4.850 % |
c |     66766 |  202535   485298 |  175259   66324  1407295    21.2 |  4.878 % |
c |     72532 |  202532   485291 |  192785   72088  1549682    21.5 |  4.879 % |
c |     81183 |  202532   485291 |  212063   80739  1802391    22.3 |  4.879 % |
c |     94157 |  202380   484941 |  233269   93661  2154388    23.0 |  4.947 % |
c |    113618 |  202380   484941 |  256596  113122  2718404    24.0 |  4.947 % |
c ==============================================================================
c [1mFound solution: 357[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    132357 |  202616   485526 |   67538  131861  3547880    26.9 |  4.947 % |
c |    132457 |  202616   485526 |   74291   22469   715651    31.9 |  4.942 % |
c |    132607 |  202567   485415 |   81720   22618   717190    31.7 |  4.964 % |
c |    132833 |  202519   485302 |   89893   22841   721278    31.6 |  4.986 % |
c |    133172 |  202417   485070 |   98882   23175   726511    31.3 |  5.032 % |
c |    133678 |  202417   485070 |  108770   23681   734153    31.0 |  5.032 % |
c |    134438 |  202417   485070 |  119647   24441   745381    30.5 |  5.032 % |
c |    135577 |  202417   485070 |  131612   25580   770437    30.1 |  5.032 % |
c |    137288 |  202417   485070 |  144773   27291   796432    29.2 |  5.032 % |
c |    139850 |  202417   485070 |  159251   29853   883336    29.6 |  5.032 % |
c |    143694 |  202191   484566 |  175176   33669   945458    28.1 |  5.128 % |
c |    149461 |  202191   484566 |  192693   39436  1113693    28.2 |  5.128 % |
c |    158110 |  202104   484366 |  211963   48082  1277192    26.6 |  5.167 % |
c |    171084 |  202104   484366 |  233159   61056  1595166    26.1 |  5.167 % |
c |    190546 |  202104   484366 |  256475   80518  2225541    27.6 |  5.167 % |
c ==============================================================================
c [1mFound solution: 334[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    200645 |  202073   484317 |   67357   90596  2672519    29.5 |  5.167 % |
c |    200745 |  202073   484317 |   74092   20503   544611    26.6 |  5.269 % |
c |    200895 |  202073   484317 |   81501   20653   546522    26.5 |  5.269 % |
c |    201121 |  202073   484317 |   89652   20879   549353    26.3 |  5.269 % |
c |    201460 |  201914   483946 |   98617   21210   553386    26.1 |  5.342 % |
c |    201967 |  201872   483858 |  108479   21716   559698    25.8 |  5.358 % |
c |    202729 |  201872   483858 |  119327   22478   568831    25.3 |  5.358 % |
c |    203868 |  201872   483858 |  131259   23617   607621    25.7 |  5.358 % |
c |    205576 |  201872   483858 |  144385   25325   630272    24.9 |  5.358 % |
c |    208139 |  201831   483763 |  158824   27885   673085    24.1 |  5.377 % |
c |    211983 |  201831   483763 |  174706   31729   763066    24.0 |  5.377 % |
c |    217750 |  201831   483763 |  192177   37496  1015541    27.1 |  5.377 % |
c |    226402 |  201785   483662 |  211395   46144  1269354    27.5 |  5.397 % |
c |    239376 |  201785   483662 |  232534   59118  1608337    27.2 |  5.397 % |
c |    258837 |  201785   483662 |  255788   78579  2179490    27.7 |  5.397 % |
c |    288029 |  201785   483662 |  281366  107771  3567695    33.1 |  5.397 % |
c |    331818 |  201748   483573 |  309503  151559  6590227    43.5 |  5.415 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 18671 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.99 0.97 0.70 2/54 18667
Raw data (stat): 18667 (runsolver) R 18666 23514 23513 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 795098627 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.99 0.97 0.71 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0003 s]
Raw data (loadavg): 0.99 0.97 0.71 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0013 s]
Raw data (loadavg): 0.99 0.97 0.71 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0009 s]
Raw data (loadavg): 0.99 0.97 0.72 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0018 s]
Raw data (loadavg): 0.99 0.97 0.72 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0016 s]
Raw data (loadavg): 0.99 0.97 0.72 3/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0017 s]
Raw data (loadavg): 0.99 0.97 0.73 3/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0024 s]
Raw data (loadavg): 0.99 0.97 0.73 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0021 s]
Raw data (loadavg): 0.99 0.97 0.73 3/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.003 s]
Raw data (loadavg): 0.99 0.97 0.73 3/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.004 s]
Raw data (loadavg): 0.99 0.97 0.73 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.74 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.009 s]
Raw data (loadavg): 0.99 0.97 0.74 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.009 s]
Raw data (loadavg): 0.99 0.97 0.74 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.011 s]
Raw data (loadavg): 0.99 0.97 0.74 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.011 s]
Raw data (loadavg): 0.99 0.97 0.74 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.011 s]
Raw data (loadavg): 0.99 0.97 0.75 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.011 s]
Raw data (loadavg): 0.99 0.97 0.75 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.012 s]
Raw data (loadavg): 0.99 0.97 0.75 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.012 s]
Raw data (loadavg): 0.99 0.97 0.75 3/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.013 s]
Raw data (loadavg): 0.99 0.97 0.75 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.013 s]
Raw data (loadavg): 0.99 0.97 0.76 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.014 s]
Raw data (loadavg): 0.99 0.97 0.76 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.014 s]
Raw data (loadavg): 0.99 0.97 0.76 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.015 s]
Raw data (loadavg): 0.99 0.97 0.76 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.016 s]
Raw data (loadavg): 0.99 0.97 0.76 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.015 s]
Raw data (loadavg): 0.99 0.97 0.77 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.016 s]
Raw data (loadavg): 0.99 0.97 0.77 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.017 s]
Raw data (loadavg): 0.99 0.97 0.77 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.018 s]
Raw data (loadavg): 0.99 0.97 0.77 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.018 s]
Raw data (loadavg): 0.99 0.97 0.77 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.017 s]
Raw data (loadavg): 0.99 0.97 0.78 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.018 s]
Raw data (loadavg): 0.99 0.97 0.78 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.018 s]
Raw data (loadavg): 0.99 0.97 0.78 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.019 s]
Raw data (loadavg): 0.99 0.97 0.78 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.02 s]
Raw data (loadavg): 0.99 0.97 0.78 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.02 s]
Raw data (loadavg): 0.99 0.97 0.79 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.025 s]
Raw data (loadavg): 0.99 0.97 0.79 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.025 s]
Raw data (loadavg): 0.99 0.97 0.79 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.026 s]
Raw data (loadavg): 0.99 0.97 0.79 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.026 s]
Raw data (loadavg): 0.99 0.97 0.79 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.026 s]
Raw data (loadavg): 0.99 0.97 0.79 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.027 s]
Raw data (loadavg): 0.99 0.97 0.80 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.026 s]
Raw data (loadavg): 0.99 0.97 0.80 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.027 s]
Raw data (loadavg): 0.99 0.97 0.80 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.027 s]
Raw data (loadavg): 0.99 0.97 0.80 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.027 s]
Raw data (loadavg): 0.99 0.97 0.80 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.028 s]
Raw data (loadavg): 0.99 0.97 0.81 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.028 s]
Raw data (loadavg): 0.99 0.97 0.81 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.029 s]
Raw data (loadavg): 0.99 0.97 0.81 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.029 s]
Raw data (loadavg): 0.99 0.97 0.81 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.029 s]
Raw data (loadavg): 0.99 0.97 0.81 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.03 s]
Raw data (loadavg): 0.99 0.97 0.82 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.031 s]
Raw data (loadavg): 0.99 0.97 0.82 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.032 s]
Raw data (loadavg): 0.99 0.97 0.82 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.033 s]
Raw data (loadavg): 0.99 0.97 0.82 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.032 s]
Raw data (loadavg): 0.99 0.97 0.82 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.033 s]
Raw data (loadavg): 0.99 0.97 0.82 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.033 s]
Raw data (loadavg): 0.99 0.97 0.82 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.034 s]
Raw data (loadavg): 0.99 0.97 0.82 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.035 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.034 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.035 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.036 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.037 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.037 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.037 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.038 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.037 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.038 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.039 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.039 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.04 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.04 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.041 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.041 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.041 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.042 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.042 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.043 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.043 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.043 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.044 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.044 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.045 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.045 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.045 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.046 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.047 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.048 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.048 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.048 s]
Raw data (loadavg): 0.99 0.97 0.86 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.049 s]
Raw data (loadavg): 0.99 0.97 0.86 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.049 s]
Raw data (loadavg): 0.99 0.97 0.86 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.05 s]
Raw data (loadavg): 0.99 0.97 0.86 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.05 s]
Raw data (loadavg): 0.99 0.97 0.86 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.05 s]
Raw data (loadavg): 0.99 0.97 0.86 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.051 s]
Raw data (loadavg): 0.99 0.97 0.86 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.051 s]
Raw data (loadavg): 0.99 0.97 0.86 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.97 0.86 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.86 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.05 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.05 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.06 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.06 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.06 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.06 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.06 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.06 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.06 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.06 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.06 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.06 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.06 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.06 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.06 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.06 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.06 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.06 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.72 s]
Raw data (loadavg): 0.99 0.97 0.89 1/53 18671
Raw data (stat): 18667 (minisat+_script) S 18666 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795098627 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.72
CPU time (s): 1229.87
CPU user time (s): 1229.21
CPU system time (s): 0.660899
CPU usage (%): 100.012
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####