PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/submitted/manquinho/primes-dimacs-cnf/normalized-ii32c3.opb
MD5SUM	00d830716ad6728e4af33fe898d69922
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	261
Optimality of the best value was proved	NO
Number of terms in the objective function	558
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	558
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	558
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03284
Number of variables	558
Total number of constraints	3551
Number of constraints which are clauses	3551
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	32
Trace number 4699

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc11 THE 2005-04-13 20:04:13 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3537 boxname=wulflinc11 idbench=153 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  00d830716ad6728e4af33fe898d69922  /oldhome/oroussel/tmp/wulflinc11/normalized-ii32c3.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc11/normalized-ii32c3.opb /oldhome/oroussel/tmp/wulflinc11/normalized-ii32c3.opb
IDLAUNCH: 3537
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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:        921112 kB
Buffers:         34084 kB
Cached:          55368 kB
SwapCached:       4932 kB
Active:          52676 kB
Inactive:        44540 kB
HighTotal:      131008 kB
HighFree:        71960 kB
LowTotal:       903652 kB
LowFree:        849152 kB
SwapTotal:     2097136 kB
SwapFree:      2092204 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            10840 kB
Committed_AS:    63476 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 20:24:15 (client local time) WITH STATUS 10 IN 1200.18 SECONDS
stats: 3537 7 1200.18 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 3551 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    3551    18021 |    1183       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 273[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1106   maxlim: 285   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        10 |   11246    45494 |    3748      10      409    40.9 |  0.000 % |
c ==============================================================================
c [1mFound solution: 266[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 292   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        42 |   11255    45542 |    3751      42     1781    42.4 |  0.000 % |
c ==============================================================================
c [1mFound solution: 265[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 293   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       114 |   11256    45552 |    3752     114     5406    47.4 |  0.000 % |
c |       214 |   11256    45552 |    4127     214     7370    34.4 |  0.538 % |
c |       364 |   11256    45552 |    4539     364    13533    37.2 |  0.538 % |
c |       590 |   11256    45552 |    4993     590    22173    37.6 |  0.538 % |
c |       927 |   11256    45552 |    5493     927    28607    30.9 |  0.538 % |
c ==============================================================================
c [1mFound solution: 264[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 294   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1230 |   11261    45579 |    3753    1230    40844    33.2 |  0.538 % |
c |      1330 |   11261    45579 |    4128    1330    41806    31.4 |  0.597 % |
c |      1480 |   11261    45579 |    4541    1480    45170    30.5 |  0.597 % |
c |      1706 |   11261    45579 |    4995    1706    53442    31.3 |  0.597 % |
c |      2045 |   11261    45579 |    5494    2045    69069    33.8 |  0.597 % |
c |      2551 |   11261    45579 |    6044    2551    95657    37.5 |  0.597 % |
c |      3312 |   11261    45579 |    6648    3312   115882    35.0 |  0.597 % |
c |      4454 |   11261    45579 |    7313    4454   182329    40.9 |  0.597 % |
c |      6166 |   11261    45579 |    8044    6166   323478    52.5 |  0.597 % |
c |      8728 |   11261    45579 |    8849    8728   487831    55.9 |  0.600 % |
c |     12572 |   11261    45579 |    9734    8085   437264    54.1 |  0.597 % |
c |     18338 |   11261    45579 |   10707    8872   506591    57.1 |  0.597 % |
c |     26988 |   11261    45579 |   11778   11514  1256666   109.1 |  0.597 % |
c |     39962 |   11261    45579 |   12956   11581  1276247   110.2 |  0.597 % |
c |     59423 |   11261    45579 |   14252    9875  1029268   104.2 |  0.597 % |
c |     88615 |   11261    45579 |   15677    8834  1189680   134.7 |  0.597 % |
c |    132404 |   11261    45579 |   17244   11128  1246087   112.0 |  0.597 % |
c |    198090 |   11261    45579 |   18969   13074  1583179   121.1 |  0.597 % |
c |    296616 |   11261    45579 |   20866   12443  1545718   124.2 |  0.597 % |
c ==============================================================================
c [1mFound solution: 263[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 295   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    335223 |   11262    45587 |    3754   17995  2148266   119.4 |  0.597 % |
c |    335323 |   11262    45587 |    4129    2350   124710    53.1 |  0.657 % |
c |    335473 |   11262    45587 |    4542    2500   134264    53.7 |  0.657 % |
c |    335698 |   11262    45587 |    4996    2725   137697    50.5 |  0.657 % |
c |    336035 |   11262    45587 |    5496    3062   156176    51.0 |  0.657 % |
c |    336541 |   11262    45587 |    6045    3568   181825    51.0 |  0.657 % |
c |    337302 |   11262    45587 |    6650    4329   240416    55.5 |  0.657 % |
c |    338445 |   11262    45587 |    7315    5472   286035    52.3 |  0.657 % |
c |    340154 |   11262    45587 |    8047    7181   421070    58.6 |  0.657 % |
c |    342717 |   11262    45587 |    8851    5636   247912    44.0 |  0.657 % |
c |    346564 |   11262    45587 |    9736    9483   738323    77.9 |  0.657 % |
c |    352330 |   11262    45587 |   10710   10369   939719    90.6 |  0.657 % |
c |    360981 |   11262    45587 |   11781    8227   539491    65.6 |  0.657 % |
c |    373955 |   11262    45587 |   12959    8242  1069805   129.8 |  0.657 % |
c |    393416 |   11233    45513 |   14255   13565  1780458   131.3 |  0.776 % |
c |    422609 |   11233    45513 |   15681   12475  1464170   117.4 |  0.776 % |
c |    466398 |   11233    45513 |   17249   14953  1525233   102.0 |  0.776 % |
c |    532084 |   11233    45513 |   18974   16973  1587234    93.5 |  0.776 % |
c |    630612 |   11233    45513 |   20871   15376  2153495   140.1 |  0.776 % |
c |    778401 |   11233    45513 |   22959   20213  2186093   108.2 |  0.780 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.97 0.89 2/54 2365
Raw data (stat): 2365 (runsolver) R 2364 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420463261 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 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.93 0.97 0.90 2/54 2365
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 1188 0 0 0 995 3 0 0 25 0 1 0 420463261 6356992 1166 4294967295 134512640 134672761 3221224576 3221223712 134565080 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1552 1166 603 41 0 1511 0
vsize: 6208
[startup+20.0018 s]
Raw data (loadavg): 0.94 0.97 0.90 2/54 2365
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 2029 0 0 0 1992 5 0 0 25 0 1 0 420463261 9838592 2007 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2402 2007 603 41 0 2361 0
vsize: 9608
[startup+30.0028 s]
Raw data (loadavg): 0.95 0.97 0.90 2/54 2365
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 2191 0 0 0 2991 6 0 0 25 0 1 0 420463261 10506240 2169 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2565 2169 603 41 0 2524 0
vsize: 10260
[startup+40.0025 s]
Raw data (loadavg): 0.96 0.97 0.90 2/54 2365
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 2236 0 0 0 3991 6 0 0 25 0 1 0 420463261 10637312 2214 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2597 2214 603 41 0 2556 0
vsize: 10388
[startup+50.003 s]
Raw data (loadavg): 0.96 0.97 0.90 2/54 2365
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 2293 0 0 0 4991 6 0 0 25 0 1 0 420463261 10903552 2271 4294967295 134512640 134672761 3221224576 3221223680 134560276 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2662 2271 603 41 0 2621 0
vsize: 10648
[startup+60.0031 s]
Raw data (loadavg): 0.97 0.97 0.90 2/54 2365
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 2448 0 0 0 5991 7 0 0 25 0 1 0 420463261 11567104 2426 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2824 2426 603 41 0 2783 0
vsize: 11296
[startup+70.0042 s]
Raw data (loadavg): 0.97 0.97 0.90 2/54 2365
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 2448 0 0 0 6990 7 0 0 25 0 1 0 420463261 11567104 2426 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2824 2426 603 41 0 2783 0
vsize: 11296
[startup+80.0044 s]
Raw data (loadavg): 0.98 0.97 0.90 2/54 2365
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 2554 0 0 0 7990 7 0 0 25 0 1 0 420463261 11968512 2532 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2922 2532 603 41 0 2881 0
vsize: 11688
[startup+90.0044 s]
Raw data (loadavg): 0.98 0.97 0.90 2/54 2365
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 3113 0 0 0 8988 9 0 0 25 0 1 0 420463261 14245888 3091 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3478 3091 603 41 0 3437 0
vsize: 13912
[startup+100.005 s]
Raw data (loadavg): 0.98 0.97 0.90 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 3131 0 0 0 9989 9 0 0 25 0 1 0 420463261 14376960 3109 4294967295 134512640 134672761 3221224576 3221223680 134560198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3510 3109 603 41 0 3469 0
vsize: 14040
[startup+110.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 3301 0 0 0 10988 9 0 0 25 0 1 0 420463261 15048704 3279 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3674 3279 603 41 0 3633 0
vsize: 14696
[startup+120.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 3301 0 0 0 11989 9 0 0 25 0 1 0 420463261 15048704 3279 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3674 3279 603 41 0 3633 0
vsize: 14696
[startup+130.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 3313 0 0 0 12989 9 0 0 25 0 1 0 420463261 15192064 3291 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3709 3291 603 41 0 3668 0
vsize: 14836
[startup+140.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 3313 0 0 0 13989 10 0 0 25 0 1 0 420463261 15192064 3291 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3709 3291 603 41 0 3668 0
vsize: 14836
[startup+150.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 3313 0 0 0 14989 10 0 0 25 0 1 0 420463261 15192064 3291 4294967295 134512640 134672761 3221224576 3221223744 134559068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3709 3291 603 41 0 3668 0
vsize: 14836
[startup+160.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 3313 0 0 0 15989 10 0 0 25 0 1 0 420463261 15192064 3291 4294967295 134512640 134672761 3221224576 3221223760 134559572 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3709 3291 603 41 0 3668 0
vsize: 14836
[startup+170.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 3314 0 0 0 16989 10 0 0 25 0 1 0 420463261 15192064 3292 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3709 3292 603 41 0 3668 0
vsize: 14836
[startup+180.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 3314 0 0 0 17989 10 0 0 25 0 1 0 420463261 15192064 3292 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3709 3292 603 41 0 3668 0
vsize: 14836
[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 3314 0 0 0 18990 10 0 0 25 0 1 0 420463261 15192064 3292 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3709 3292 603 41 0 3668 0
vsize: 14836
[startup+200.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 3327 0 0 0 19990 10 0 0 25 0 1 0 420463261 15192064 3305 4294967295 134512640 134672761 3221224576 3221223680 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3709 3305 603 41 0 3668 0
vsize: 14836
[startup+210.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 3382 0 0 0 20990 10 0 0 25 0 1 0 420463261 15462400 3360 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3775 3360 603 41 0 3734 0
vsize: 15100
[startup+220.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 3382 0 0 0 21990 10 0 0 25 0 1 0 420463261 15462400 3360 4294967295 134512640 134672761 3221224576 3221223584 1075349746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3775 3360 603 41 0 3734 0
vsize: 15100
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 3382 0 0 0 22990 10 0 0 25 0 1 0 420463261 15462400 3360 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3775 3360 603 41 0 3734 0
vsize: 15100
[startup+240.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 3382 0 0 0 23990 10 0 0 25 0 1 0 420463261 15429632 3360 4294967295 134512640 134672761 3221224576 3221223680 134560376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3767 3360 603 41 0 3726 0
vsize: 15068
[startup+250.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 3402 0 0 0 24990 10 0 0 25 0 1 0 420463261 15429632 3380 4294967295 134512640 134672761 3221224576 3221223744 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3767 3380 603 41 0 3726 0
vsize: 15068
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 3404 0 0 0 25990 10 0 0 25 0 1 0 420463261 15429632 3382 4294967295 134512640 134672761 3221224576 3221223680 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3767 3382 603 41 0 3726 0
vsize: 15068
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 3404 0 0 0 26990 10 0 0 25 0 1 0 420463261 15429632 3382 4294967295 134512640 134672761 3221224576 3221223760 134559345 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3767 3382 603 41 0 3726 0
vsize: 15068
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 3404 0 0 0 27990 10 0 0 25 0 1 0 420463261 15429632 3382 4294967295 134512640 134672761 3221224576 3221223680 134560287 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3767 3382 603 41 0 3726 0
vsize: 15068
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 3690 0 0 0 28990 11 0 0 25 0 1 0 420463261 16633856 3668 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4061 3668 603 41 0 4020 0
vsize: 16244
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 3780 0 0 0 29989 11 0 0 25 0 1 0 420463261 17031168 3758 4294967295 134512640 134672761 3221224576 3221223680 134560267 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4158 3758 603 41 0 4117 0
vsize: 16632
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 3790 0 0 0 30990 11 0 0 25 0 1 0 420463261 17031168 3768 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4158 3768 603 41 0 4117 0
vsize: 16632
[startup+320.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 3790 0 0 0 31990 11 0 0 25 0 1 0 420463261 17031168 3768 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4158 3768 603 41 0 4117 0
vsize: 16632
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 3854 0 0 0 32990 11 0 0 25 0 1 0 420463261 17297408 3832 4294967295 134512640 134672761 3221224576 3221223680 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4223 3832 603 41 0 4182 0
vsize: 16892
[startup+340.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 3854 0 0 0 33990 11 0 0 25 0 1 0 420463261 17297408 3832 4294967295 134512640 134672761 3221224576 3221223648 134553544 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4223 3832 603 41 0 4182 0
vsize: 16892
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 3854 0 0 0 34990 11 0 0 25 0 1 0 420463261 17297408 3832 4294967295 134512640 134672761 3221224576 3221223744 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4223 3832 603 41 0 4182 0
vsize: 16892
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 3854 0 0 0 35990 11 0 0 25 0 1 0 420463261 17297408 3832 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4223 3832 603 41 0 4182 0
vsize: 16892
[startup+370.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 3939 0 0 0 36990 12 0 0 25 0 1 0 420463261 17702912 3917 4294967295 134512640 134672761 3221224576 3221223680 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4322 3917 603 41 0 4281 0
vsize: 17288
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 3943 0 0 0 37991 12 0 0 25 0 1 0 420463261 17702912 3921 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4322 3921 603 41 0 4281 0
vsize: 17288
[startup+390.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4132 0 0 0 38990 12 0 0 25 0 1 0 420463261 18501632 4110 4294967295 134512640 134672761 3221224576 3221223712 134565116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4517 4110 603 41 0 4476 0
vsize: 18068
[startup+400.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4132 0 0 0 39990 12 0 0 25 0 1 0 420463261 18501632 4110 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4517 4110 603 41 0 4476 0
vsize: 18068
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4132 0 0 0 40990 12 0 0 25 0 1 0 420463261 18501632 4110 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4517 4110 603 41 0 4476 0
vsize: 18068
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4132 0 0 0 41991 12 0 0 25 0 1 0 420463261 18501632 4110 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4517 4110 603 41 0 4476 0
vsize: 18068
[startup+430.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4132 0 0 0 42991 12 0 0 25 0 1 0 420463261 18501632 4110 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4517 4110 603 41 0 4476 0
vsize: 18068
[startup+440.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4134 0 0 0 43990 12 0 0 25 0 1 0 420463261 18501632 4112 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4517 4112 603 41 0 4476 0
vsize: 18068
[startup+450.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4134 0 0 0 44991 12 0 0 25 0 1 0 420463261 18501632 4112 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4517 4112 603 41 0 4476 0
vsize: 18068
[startup+460.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4134 0 0 0 45991 12 0 0 25 0 1 0 420463261 18501632 4112 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4517 4112 603 41 0 4476 0
vsize: 18068
[startup+470.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4134 0 0 0 46991 12 0 0 25 0 1 0 420463261 18501632 4112 4294967295 134512640 134672761 3221224576 3221223744 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4517 4112 603 41 0 4476 0
vsize: 18068
[startup+480.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4134 0 0 0 47991 12 0 0 25 0 1 0 420463261 18501632 4112 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4517 4112 603 41 0 4476 0
vsize: 18068
[startup+490.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4134 0 0 0 48991 12 0 0 25 0 1 0 420463261 18501632 4112 4294967295 134512640 134672761 3221224576 3221223680 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4517 4112 603 41 0 4476 0
vsize: 18068
[startup+500.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4134 0 0 0 49992 12 0 0 25 0 1 0 420463261 18501632 4112 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4517 4112 603 41 0 4476 0
vsize: 18068
[startup+510.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4134 0 0 0 50992 12 0 0 25 0 1 0 420463261 18501632 4112 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4517 4112 603 41 0 4476 0
vsize: 18068
[startup+520.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4134 0 0 0 51992 12 0 0 25 0 1 0 420463261 18501632 4112 4294967295 134512640 134672761 3221224576 3221223748 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4517 4112 603 41 0 4476 0
vsize: 18068
[startup+530.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4134 0 0 0 52992 12 0 0 25 0 1 0 420463261 18501632 4112 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4517 4112 603 41 0 4476 0
vsize: 18068
[startup+540.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4134 0 0 0 53992 12 0 0 25 0 1 0 420463261 18501632 4112 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4517 4112 603 41 0 4476 0
vsize: 18068
[startup+550.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4134 0 0 0 54993 12 0 0 25 0 1 0 420463261 18501632 4112 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4517 4112 603 41 0 4476 0
vsize: 18068
[startup+560.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4134 0 0 0 55993 12 0 0 25 0 1 0 420463261 18501632 4112 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4517 4112 603 41 0 4476 0
vsize: 18068
[startup+570.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4134 0 0 0 56993 12 0 0 25 0 1 0 420463261 18501632 4112 4294967295 134512640 134672761 3221224576 3221223744 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4517 4112 603 41 0 4476 0
vsize: 18068
[startup+580.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4134 0 0 0 57993 12 0 0 25 0 1 0 420463261 18501632 4112 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4517 4112 603 41 0 4476 0
vsize: 18068
[startup+590.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4134 0 0 0 58993 12 0 0 25 0 1 0 420463261 18501632 4112 4294967295 134512640 134672761 3221224576 3221223760 134559365 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4517 4112 603 41 0 4476 0
vsize: 18068
[startup+600.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4134 0 0 0 59993 12 0 0 25 0 1 0 420463261 18501632 4112 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4517 4112 603 41 0 4476 0
vsize: 18068
[startup+610.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4134 0 0 0 60994 12 0 0 25 0 1 0 420463261 18501632 4112 4294967295 134512640 134672761 3221224576 3221223680 134559805 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4517 4112 603 41 0 4476 0
vsize: 18068
[startup+620.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4134 0 0 0 61994 12 0 0 25 0 1 0 420463261 18501632 4112 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4517 4112 603 41 0 4476 0
vsize: 18068
[startup+630.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4134 0 0 0 62994 12 0 0 25 0 1 0 420463261 18501632 4112 4294967295 134512640 134672761 3221224576 3221223744 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4517 4112 603 41 0 4476 0
vsize: 18068
[startup+640.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4134 0 0 0 63994 12 0 0 25 0 1 0 420463261 18501632 4112 4294967295 134512640 134672761 3221224576 3221223632 134565137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4517 4112 603 41 0 4476 0
vsize: 18068
[startup+650.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4134 0 0 0 64994 12 0 0 25 0 1 0 420463261 18501632 4112 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4517 4112 603 41 0 4476 0
vsize: 18068
[startup+660.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4134 0 0 0 65995 12 0 0 25 0 1 0 420463261 18501632 4112 4294967295 134512640 134672761 3221224576 3221223680 134559910 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4517 4112 603 41 0 4476 0
vsize: 18068
[startup+670.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4134 0 0 0 66995 12 0 0 25 0 1 0 420463261 18501632 4112 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4517 4112 603 41 0 4476 0
vsize: 18068
[startup+680.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4134 0 0 0 67995 12 0 0 25 0 1 0 420463261 18501632 4112 4294967295 134512640 134672761 3221224576 3221223680 134560379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4517 4112 603 41 0 4476 0
vsize: 18068
[startup+690.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4134 0 0 0 68995 12 0 0 25 0 1 0 420463261 18501632 4112 4294967295 134512640 134672761 3221224576 3221223760 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4517 4112 603 41 0 4476 0
vsize: 18068
[startup+700.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4134 0 0 0 69995 12 0 0 25 0 1 0 420463261 18501632 4112 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4517 4112 603 41 0 4476 0
vsize: 18068
[startup+710.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4134 0 0 0 70996 12 0 0 25 0 1 0 420463261 18501632 4112 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4517 4112 603 41 0 4476 0
vsize: 18068
[startup+720.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4134 0 0 0 71996 12 0 0 25 0 1 0 420463261 18501632 4112 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4517 4112 603 41 0 4476 0
vsize: 18068
[startup+730.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4134 0 0 0 72996 12 0 0 25 0 1 0 420463261 18501632 4112 4294967295 134512640 134672761 3221224576 3221223680 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4517 4112 603 41 0 4476 0
vsize: 18068
[startup+740.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4134 0 0 0 73996 12 0 0 25 0 1 0 420463261 18501632 4112 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4517 4112 603 41 0 4476 0
vsize: 18068
[startup+750.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4134 0 0 0 74996 12 0 0 25 0 1 0 420463261 18501632 4112 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4517 4112 603 41 0 4476 0
vsize: 18068
[startup+760.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4134 0 0 0 75997 12 0 0 25 0 1 0 420463261 18501632 4112 4294967295 134512640 134672761 3221224576 3221223744 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4517 4112 603 41 0 4476 0
vsize: 18068
[startup+770.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4134 0 0 0 76997 12 0 0 25 0 1 0 420463261 18501632 4112 4294967295 134512640 134672761 3221224576 3221223728 134542672 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4517 4112 603 41 0 4476 0
vsize: 18068
[startup+780.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4134 0 0 0 77997 12 0 0 25 0 1 0 420463261 18501632 4112 4294967295 134512640 134672761 3221224576 3221223680 134560344 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4517 4112 603 41 0 4476 0
vsize: 18068
[startup+790.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4326 0 0 0 78997 13 0 0 25 0 1 0 420463261 19300352 4304 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4712 4304 603 41 0 4671 0
vsize: 18848
[startup+800.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4326 0 0 0 79997 13 0 0 25 0 1 0 420463261 19300352 4304 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4712 4304 603 41 0 4671 0
vsize: 18848
[startup+810.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4681 0 0 0 80996 14 0 0 25 0 1 0 420463261 20779008 4659 4294967295 134512640 134672761 3221224576 3221223680 134560191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5073 4659 603 41 0 5032 0
vsize: 20292
[startup+820.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4681 0 0 0 81996 14 0 0 25 0 1 0 420463261 20779008 4659 4294967295 134512640 134672761 3221224576 3221223680 134560229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5073 4659 603 41 0 5032 0
vsize: 20292
[startup+830.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4681 0 0 0 82996 14 0 0 25 0 1 0 420463261 20770816 4659 4294967295 134512640 134672761 3221224576 3221223680 134559838 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5071 4659 603 41 0 5030 0
vsize: 20284
[startup+840.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4681 0 0 0 83996 14 0 0 25 0 1 0 420463261 20770816 4659 4294967295 134512640 134672761 3221224576 3221223680 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5071 4659 603 41 0 5030 0
vsize: 20284
[startup+850.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4681 0 0 0 84996 14 0 0 25 0 1 0 420463261 20770816 4659 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5071 4659 603 41 0 5030 0
vsize: 20284
[startup+860.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4681 0 0 0 85997 14 0 0 25 0 1 0 420463261 20770816 4659 4294967295 134512640 134672761 3221224576 3221223760 134558629 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5071 4659 603 41 0 5030 0
vsize: 20284
[startup+870.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4681 0 0 0 86997 14 0 0 25 0 1 0 420463261 20762624 4659 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5069 4659 603 41 0 5028 0
vsize: 20276
[startup+880.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4681 0 0 0 87997 14 0 0 25 0 1 0 420463261 20762624 4659 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5069 4659 603 41 0 5028 0
vsize: 20276
[startup+890.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4681 0 0 0 88997 14 0 0 25 0 1 0 420463261 20762624 4659 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5069 4659 603 41 0 5028 0
vsize: 20276
[startup+900.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4681 0 0 0 89997 14 0 0 25 0 1 0 420463261 20762624 4659 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5069 4659 603 41 0 5028 0
vsize: 20276
[startup+910.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4681 0 0 0 90998 14 0 0 25 0 1 0 420463261 20762624 4659 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5069 4659 603 41 0 5028 0
vsize: 20276
[startup+920.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4681 0 0 0 91998 14 0 0 25 0 1 0 420463261 20762624 4659 4294967295 134512640 134672761 3221224576 3221223680 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5069 4659 603 41 0 5028 0
vsize: 20276
[startup+930.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4681 0 0 0 92998 14 0 0 25 0 1 0 420463261 20762624 4659 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5069 4659 603 41 0 5028 0
vsize: 20276
[startup+940.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4688 0 0 0 93998 14 0 0 25 0 1 0 420463261 20762624 4666 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5069 4666 603 41 0 5028 0
vsize: 20276
[startup+950.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4688 0 0 0 94997 15 0 0 25 0 1 0 420463261 20762624 4666 4294967295 134512640 134672761 3221224576 3221223760 134559622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5069 4666 603 41 0 5028 0
vsize: 20276
[startup+960.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4688 0 0 0 95997 15 0 0 25 0 1 0 420463261 20762624 4666 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5069 4666 603 41 0 5028 0
vsize: 20276
[startup+970.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4688 0 0 0 96998 15 0 0 25 0 1 0 420463261 20762624 4666 4294967295 134512640 134672761 3221224576 3221223680 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5069 4666 603 41 0 5028 0
vsize: 20276
[startup+980.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4688 0 0 0 97998 15 0 0 25 0 1 0 420463261 20762624 4666 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5069 4666 603 41 0 5028 0
vsize: 20276
[startup+990.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4688 0 0 0 98998 15 0 0 25 0 1 0 420463261 20762624 4666 4294967295 134512640 134672761 3221224576 3221223680 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5069 4666 603 41 0 5028 0
vsize: 20276
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4688 0 0 0 99998 15 0 0 25 0 1 0 420463261 20762624 4666 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5069 4666 603 41 0 5028 0
vsize: 20276
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4688 0 0 0 100998 15 0 0 25 0 1 0 420463261 20762624 4666 4294967295 134512640 134672761 3221224576 3221223744 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5069 4666 603 41 0 5028 0
vsize: 20276
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4688 0 0 0 101998 15 0 0 25 0 1 0 420463261 20762624 4666 4294967295 134512640 134672761 3221224576 3221223744 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5069 4666 603 41 0 5028 0
vsize: 20276
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4697 0 0 0 102999 15 0 0 25 0 1 0 420463261 20762624 4675 4294967295 134512640 134672761 3221224576 3221223760 134558930 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5069 4675 603 41 0 5028 0
vsize: 20276
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4702 0 0 0 103999 15 0 0 25 0 1 0 420463261 20762624 4680 4294967295 134512640 134672761 3221224576 3221223680 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5069 4680 603 41 0 5028 0
vsize: 20276
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4702 0 0 0 104999 15 0 0 25 0 1 0 420463261 20762624 4680 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5069 4680 603 41 0 5028 0
vsize: 20276
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4702 0 0 0 105999 15 0 0 25 0 1 0 420463261 20762624 4680 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5069 4680 603 41 0 5028 0
vsize: 20276
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4702 0 0 0 106999 15 0 0 25 0 1 0 420463261 20762624 4680 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5069 4680 603 41 0 5028 0
vsize: 20276
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4702 0 0 0 107999 15 0 0 25 0 1 0 420463261 20762624 4680 4294967295 134512640 134672761 3221224576 3221223700 134566118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5069 4680 603 41 0 5028 0
vsize: 20276
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4702 0 0 0 109000 15 0 0 25 0 1 0 420463261 20762624 4680 4294967295 134512640 134672761 3221224576 3221223680 134560287 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5069 4680 603 41 0 5028 0
vsize: 20276
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4702 0 0 0 110000 15 0 0 25 0 1 0 420463261 20762624 4680 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5069 4680 603 41 0 5028 0
vsize: 20276
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4702 0 0 0 111000 15 0 0 25 0 1 0 420463261 20762624 4680 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5069 4680 603 41 0 5028 0
vsize: 20276
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4702 0 0 0 112000 15 0 0 25 0 1 0 420463261 20762624 4680 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5069 4680 603 41 0 5028 0
vsize: 20276
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4702 0 0 0 113000 15 0 0 25 0 1 0 420463261 20762624 4680 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5069 4680 603 41 0 5028 0
vsize: 20276
[startup+1140.03 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4702 0 0 0 114001 15 0 0 25 0 1 0 420463261 20762624 4680 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5069 4680 603 41 0 5028 0
vsize: 20276
[startup+1150.03 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4702 0 0 0 115001 15 0 0 25 0 1 0 420463261 20762624 4680 4294967295 134512640 134672761 3221224576 3221223744 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5069 4680 603 41 0 5028 0
vsize: 20276
[startup+1160.03 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4702 0 0 0 116001 15 0 0 25 0 1 0 420463261 20762624 4680 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5069 4680 603 41 0 5028 0
vsize: 20276
[startup+1170.03 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4702 0 0 0 117001 15 0 0 25 0 1 0 420463261 20762624 4680 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5069 4680 603 41 0 5028 0
vsize: 20276
[startup+1180.03 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4702 0 0 0 118001 15 0 0 25 0 1 0 420463261 20762624 4680 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5069 4680 603 41 0 5028 0
vsize: 20276
[startup+1190.03 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4704 0 0 0 119001 15 0 0 25 0 1 0 420463261 20762624 4682 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5069 4682 603 41 0 5028 0
vsize: 20276
[startup+1200.03 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 2367
Raw data (stat): 2365 (minisat+) R 2364 32461 32460 0 -1 0 4704 0 0 0 120001 15 0 0 25 0 1 0 420463261 20762624 4682 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5069 4682 603 41 0 5028 0
vsize: 20276
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 1.02 0.99 0.91 1/54 2367
Raw data (stat): 2365 (minisat+) Z 2364 32461 32460 0 -1 12 4707 0 0 0 120001 16 0 0 25 0 1 0 420463261 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.05
CPU time (s): 1200.18
CPU user time (s): 1200.01
CPU system time (s): 0.166974
CPU usage (%): 100.011
Max. virtual memory (Kb): 20292
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####