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/mps-v2-13-7/plato.asu.edu/pub/fctp/normalized-mps-v2-13-7-ran10x12.opb
MD5SUM	ddd1f838c1e3a248aad1987162b1d40d
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	656964
Optimality of the best value was proved	NO
Number of terms in the objective function	2520
Biggest coefficient in the objective function	5242880
Number of bits for the biggest coefficient in the objective function	23
Sum of the numbers in the objective function	666682247
Number of bits of the sum of numbers in the objective function	30
Biggest number in a constraint	5242880
Number of bits of the biggest number in a constraint	23
Biggest sum of numbers in a constraint	666682247
Number of bits of the biggest sum of numbers	30
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.04
Number of variables	2520
Total number of constraints	142
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	142
Minimum length of a constraint	21
Maximum length of a constraint	240
Trace number 32444

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-05-27 09:59:21 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=23836 boxname=wulflinc3 idbench=1480 idsolver=16 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ddd1f838c1e3a248aad1987162b1d40d  /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-ran10x12.opb
REAL COMMAND:  minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-ran10x12.opb
IDLAUNCH: 23836
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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		: 451.190
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:        859268 kB
Buffers:         30472 kB
Cached:         124956 kB
SwapCached:         20 kB
Active:          31552 kB
Inactive:       126592 kB
HighTotal:      131008 kB
HighFree:         4536 kB
LowTotal:       903652 kB
LowFree:        854732 kB
SwapTotal:     2097136 kB
SwapFree:      2096780 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6584 kB
Slab:            11472 kB
Committed_AS:    71792 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-27 10:19:51 (client local time) WITH STATUS 152 IN 1229.89 SECONDS
stats: 23836 7 1229.89 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 164 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ######################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 162]---> BDD-cost: 1548
c ---[ 160]---> BDD-cost: 1646
c ---[ 158]---> BDD-cost: 1716
c ---[ 156]---> BDD-cost: 1601
c ---[ 154]---> BDD-cost: 1418
c ---[ 152]---> BDD-cost: 1472
c ---[ 150]---> BDD-cost: 1708
c ---[ 148]---> BDD-cost: 1281
c ---[ 146]---> BDD-cost: 1281
c ---[ 144]---> BDD-cost: 1517
c ---[ 142]---> BDD-cost:  750
c ---[ 140]---> BDD-cost:  983
c ---[ 138]---> BDD-cost:  927
c ---[ 136]---> BDD-cost: 1311
c ---[ 134]---> BDD-cost: 1109
c ---[ 132]---> BDD-cost:  817
c ---[ 130]---> BDD-cost: 1253
c ---[ 128]---> BDD-cost: 1167
c ---[ 126]---> BDD-cost:  750
c ---[ 124]---> BDD-cost:  750
c ---[ 122]---> BDD-cost: 1253
c ---[ 120]---> BDD-cost:  750
c ---[ 119]---> BDD-cost:   10
c ---[ 118]---> BDD-cost:   13
c ---[ 117]---> BDD-cost:   13
c ---[ 116]---> BDD-cost:   13
c ---[ 115]---> BDD-cost:   13
c ---[ 114]---> BDD-cost:   10
c ---[ 113]---> BDD-cost:   10
c ---[ 112]---> BDD-cost:   13
c ---[ 111]---> BDD-cost:   10
c ---[ 110]---> BDD-cost:   13
c ---[ 109]---> BDD-cost:   13
c ---[ 108]---> BDD-cost:   10
c ---[ 107]---> BDD-cost:   13
c ---[ 106]---> BDD-cost:   14
c ---[ 105]---> BDD-cost:   13
c ---[ 104]---> BDD-cost:   11
c ---[ 103]---> BDD-cost:   13
c ---[ 102]---> BDD-cost:   13
c ---[ 101]---> BDD-cost:   10
c ---[ 100]---> BDD-cost:   10
c ---[  99]---> BDD-cost:   13
c ---[  98]---> BDD-cost:   10
c ---[  97]---> BDD-cost:   13
c ---[  96]---> BDD-cost:   13
c ---[  95]---> BDD-cost:   10
c ---[  94]---> BDD-cost:   13
c ---[  93]---> BDD-cost:   15
c ---[  92]---> BDD-cost:   11
c ---[  91]---> BDD-cost:   17
c ---[  90]---> BDD-cost:   13
c ---[  89]---> BDD-cost:   10
c ---[  88]---> BDD-cost:   10
c ---[  87]---> BDD-cost:   15
c ---[  86]---> BDD-cost:   17
c ---[  85]---> BDD-cost:   10
c ---[  84]---> BDD-cost:   13
c ---[  83]---> BDD-cost:   17
c ---[  82]---> BDD-cost:   10
c ---[  81]---> BDD-cost:   13
c ---[  80]---> BDD-cost:   15
c ---[  79]---> BDD-cost:   11
c ---[  78]---> BDD-cost:   15
c ---[  77]---> BDD-cost:   13
c ---[  76]---> BDD-cost:   11
c ---[  75]---> BDD-cost:   10
c ---[  74]---> BDD-cost:   10
c ---[  73]---> BDD-cost:   17
c ---[  72]---> BDD-cost:   10
c ---[  71]---> BDD-cost:   13
c ---[  70]---> BDD-cost:   16
c ---[  69]---> BDD-cost:   10
c ---[  68]---> BDD-cost:   13
c ---[  67]---> BDD-cost:   15
c ---[  66]---> BDD-cost:   11
c ---[  65]---> BDD-cost:   14
c ---[  64]---> BDD-cost:   17
c ---[  63]---> BDD-cost:   13
c ---[  62]---> BDD-cost:   10
c ---[  61]---> BDD-cost:   10
c ---[  60]---> BDD-cost:   17
c ---[  59]---> BDD-cost:   10
c ---[  58]---> BDD-cost:   13
c ---[  57]---> BDD-cost:   17
c ---[  56]---> BDD-cost:   10
c ---[  55]---> BDD-cost:   13
c ---[  54]---> BDD-cost:   14
c ---[  53]---> BDD-cost:   12
c ---[  52]---> BDD-cost:   11
c ---[  51]---> BDD-cost:   12
c ---[  50]---> BDD-cost:   12
c ---[  49]---> BDD-cost:   10
c ---[  48]---> BDD-cost:   10
c ---[  47]---> BDD-cost:   12
c ---[  46]---> BDD-cost:   10
c ---[  45]---> BDD-cost:   13
c ---[  44]---> BDD-cost:   12
c ---[  43]---> BDD-cost:   10
c ---[  42]---> BDD-cost:   10
c ---[  41]---> BDD-cost:   13
c ---[  40]---> BDD-cost:   14
c ---[  39]---> BDD-cost:   11
c ---[  38]---> BDD-cost:   14
c ---[  37]---> BDD-cost:   14
c ---[  36]---> BDD-cost:   10
c ---[  35]---> BDD-cost:   10
c ---[  34]---> BDD-cost:   14
c ---[  33]---> BDD-cost:   10
c ---[  32]---> BDD-cost:   10
c ---[  31]---> BDD-cost:   13
c ---[  30]---> BDD-cost:   14
c ---[  29]---> BDD-cost:   10
c ---[  28]---> BDD-cost:   13
c ---[  27]---> BDD-cost:   15
c ---[  26]---> BDD-cost:   11
c ---[  25]---> BDD-cost:   15
c ---[  24]---> BDD-cost:   13
c ---[  23]---> BDD-cost:   10
c ---[  22]---> BDD-cost:   10
c ---[  21]---> BDD-cost:   14
c ---[  20]---> BDD-cost:   15
c ---[  19]---> BDD-cost:   10
c ---[  18]---> BDD-cost:   13
c ---[  17]---> BDD-cost:   15
c ---[  16]---> BDD-cost:   10
c ---[  15]---> BDD-cost:   13
c ---[  14]---> BDD-cost:   13
c ---[  13]---> BDD-cost:   11
c ---[  12]---> BDD-cost:   13
c ---[  11]---> BDD-cost:   13
c ---[  10]---> BDD-cost:   10
c ---[   9]---> BDD-cost:   10
c ---[   8]---> BDD-cost:   10
c ---[   7]---> BDD-cost:   13
c ---[   6]---> BDD-cost:   10
c ---[   5]---> BDD-cost:   13
c ---[   4]---> BDD-cost:   13
c ---[   3]---> BDD-cost:   10
c ---[   2]---> BDD-cost:   13
c ---[   1]---> BDD-cost:   13
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   78831   227645 |   26277       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 3054313[0m
c ---[   0]---> Sorter-cost:185471     Base: 2 2 2 2 2 2 2 2 2 2 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        68 |  589649  1420169 |  196549      68     1902    28.0 |  0.000 % |
c |       169 |  589649  1420169 |  216203     169     6970    41.2 |  0.649 % |
c |       319 |  589649  1420169 |  237824     319     8741    27.4 |  0.649 % |
c |       545 |  589649  1420169 |  261606     545     9958    18.3 |  0.649 % |
c |       882 |  589649  1420169 |  287767     882    16735    19.0 |  0.649 % |
c |      1388 |  589649  1420169 |  316544    1388    21196    15.3 |  0.649 % |
c |      2147 |  589649  1420169 |  348198    2147    27474    12.8 |  0.649 % |
c |      3286 |  589649  1420169 |  383018    3286    41414    12.6 |  0.649 % |
c |      4995 |  589649  1420169 |  421320    4995    64507    12.9 |  0.649 % |
c |      7557 |  589622  1420109 |  463452    7556   307002    40.6 |  0.652 % |
c |     11402 |  589622  1420109 |  509797   11401   528565    46.4 |  0.652 % |
c |     17170 |  589622  1420109 |  560777   17169   614737    35.8 |  0.652 % |
c |     25820 |  589622  1420109 |  616854   25819   746318    28.9 |  0.652 % |
c |     38798 |  589622  1420109 |  678540   38797  1117923    28.8 |  0.652 % |
c |     58259 |  589622  1420109 |  746394   58258  1596464    27.4 |  0.652 % |
c ==============================================================================
c [1mFound solution: 2427718[0m
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     83034 |  590560  1423180 |  196853   83032  2608650    31.4 |  0.652 % |
c |     83134 |  590560  1423180 |  216538   83132  2613962    31.4 |  0.653 % |
c |     83285 |  590560  1423180 |  238192   83283  2627122    31.5 |  0.653 % |
c |     83511 |  590560  1423180 |  262011   83509  2631477    31.5 |  0.653 % |
c |     83848 |  590560  1423180 |  288212   83846  2633250    31.4 |  0.653 % |
c |     84354 |  590560  1423180 |  317033   84352  2636705    31.3 |  0.653 % |
c |     85113 |  590560  1423180 |  348737   85111  2646139    31.1 |  0.653 % |
c ==============================================================================
c [1mFound solution: 1681961[0m
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86243 |  592093  1426988 |  197364   86235  2685938    31.1 |  0.653 % |
c |     86343 |  592027  1426839 |  217100   86334  2687709    31.1 |  0.677 % |
c |     86494 |  592027  1426839 |  238810   86485  2696180    31.2 |  0.677 % |
c |     86720 |  591801  1426329 |  262691   86710  2703028    31.2 |  0.706 % |
c |     87057 |  591568  1425803 |  288960   87043  2717799    31.2 |  0.736 % |
c |     87565 |  591427  1425483 |  317856   87550  2720646    31.1 |  0.754 % |
c |     88324 |  591427  1425483 |  349642   88309  2726432    30.9 |  0.754 % |
c |     89464 |  591124  1424796 |  384606   89438  2781184    31.1 |  0.794 % |
c |     91172 |  590907  1424301 |  423067   91144  2829207    31.0 |  0.826 % |
c |     93734 |  590907  1424301 |  465373   93706  2910167    31.1 |  0.826 % |
c |     97579 |  590895  1424274 |  511911   97550  2972855    30.5 |  0.827 % |
c |    103345 |  590895  1424274 |  563102  103316  3806125    36.8 |  0.827 % |
c |    111994 |  590129  1422526 |  619412  111956  5945004    53.1 |  0.933 % |
c |    124968 |  590129  1422526 |  681354  124930  8086181    64.7 |  0.933 % |
c |    144430 |  590129  1422526 |  749489  144392  9595759    66.5 |  0.933 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 13723 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.90 0.93 0.90 2/54 13719
Raw data (stat): 13719 (runsolver) R 13718 20224 20223 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 797039283 1052672 99 4294967295 134512640 135381576 3221224464 3221219672 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.91 0.94 0.90 2/55 13723
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.0027 s]
Raw data (loadavg): 0.92 0.94 0.91 2/55 13723
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.0037 s]
Raw data (loadavg): 0.94 0.94 0.91 2/55 13723
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.0039 s]
Raw data (loadavg): 0.94 0.94 0.91 2/55 13723
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.0046 s]
Raw data (loadavg): 1.03 0.96 0.91 2/55 13776
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.005 s]
Raw data (loadavg): 1.03 0.96 0.91 2/55 13776
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.0052 s]
Raw data (loadavg): 1.02 0.96 0.91 2/55 13776
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.0064 s]
Raw data (loadavg): 1.02 0.96 0.91 2/55 13776
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.0065 s]
Raw data (loadavg): 1.02 0.96 0.91 2/55 13776
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.007 s]
Raw data (loadavg): 1.01 0.96 0.91 2/55 13776
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.008 s]
Raw data (loadavg): 1.01 0.97 0.91 2/55 13776
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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): 1.01 0.97 0.91 2/55 13778
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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): 1.01 0.97 0.91 2/55 13778
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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): 1.00 0.97 0.91 2/55 13778
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13778
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13778
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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): 1.00 0.97 0.91 2/55 13778
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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): 1.00 0.97 0.91 2/55 13778
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13778
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13778
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13778
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13778
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13778
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13778
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13778
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13778
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13778
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13778
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13778
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13778
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13778
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13778
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13778
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13778
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.023 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.032 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.031 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.031 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.032 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.031 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.032 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.032 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.033 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.033 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.032 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.033 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.034 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.034 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.034 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.034 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.034 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.034 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.035 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.036 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.036 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.036 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.036 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.037 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.038 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.038 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.038 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.038 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.041 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.041 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.041 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.042 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.042 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.043 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.044 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.044 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.044 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.045 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.045 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.046 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.046 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.047 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.046 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.047 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.048 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.75 s]
Raw data (loadavg): 1.00 0.97 0.91 1/53 13780
Raw data (stat): 13719 (minisat+_script) S 13718 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797039283 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.75
CPU time (s): 1229.89
CPU user time (s): 1228.99
CPU system time (s): 0.897863
CPU usage (%): 100.011
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####