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/synthesis-ptl-cmos-circuits/normalized-cm42a.opb
MD5SUM	62b75258091a8b1382fa8b1c633d9511
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	694
Optimality of the best value was proved	NO
Number of terms in the objective function	99
Biggest coefficient in the objective function	60
Number of bits for the biggest coefficient in the objective function	6
Sum of the numbers in the objective function	4087
Number of bits of the sum of numbers in the objective function	12
Biggest number in a constraint	60
Number of bits of the biggest number in a constraint	6
Biggest sum of numbers in a constraint	4087
Number of bits of the biggest sum of numbers	12
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	0.168973
Number of variables	99
Total number of constraints	185
Number of constraints which are clauses	185
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	20
Trace number 5208

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc2 THE 2005-04-13 22:30:15 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3636 boxname=wulflinc2 idbench=252 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  62b75258091a8b1382fa8b1c633d9511  /oldhome/oroussel/tmp/wulflinc2/normalized-cm42a.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc2/normalized-cm42a.opb /oldhome/oroussel/tmp/wulflinc2/normalized-cm42a.opb
IDLAUNCH: 3636
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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.191
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:        907612 kB
Buffers:         33772 kB
Cached:          72916 kB
SwapCached:          4 kB
Active:          54932 kB
Inactive:        54548 kB
HighTotal:      131008 kB
HighFree:        54376 kB
LowTotal:       903652 kB
LowFree:        853236 kB
SwapTotal:     2097136 kB
SwapFree:      2097132 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            11964 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 22:50:17 (client local time) WITH STATUS 10 IN 1200.16 SECONDS
stats: 3636 7 1200.16 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 185 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 |     185      626 |      61       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 939[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 464   maxlim: 3148   bits: 12/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    3395    12099 |    1131       0        0     nan |  0.000 % |
c |       100 |    3265    11727 |    1244      96      569     5.9 |  2.289 % |
c |       250 |    3249    11675 |    1368     242     2794    11.5 |  2.819 % |
c ==============================================================================
c [1mFound solution: 915[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 306   maxlim: 3172   bits: 12/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       288 |    5334    19113 |    1778     280     3460    12.4 |  2.819 % |
c |       390 |    5334    19113 |    1955     382     4464    11.7 |  2.617 % |
c |       540 |    5334    19113 |    2151     532     5813    10.9 |  2.617 % |
c |       766 |    5334    19113 |    2366     758    15322    20.2 |  2.617 % |
c |      1103 |    5334    19113 |    2603    1095    19512    17.8 |  2.617 % |
c |      1609 |    5334    19113 |    2863    1601    33897    21.2 |  2.617 % |
c |      2368 |    5334    19113 |    3149    2360    66005    28.0 |  2.617 % |
c |      3507 |    5334    19113 |    3464    1857    45662    24.6 |  2.617 % |
c ==============================================================================
c [1mFound solution: 857[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3230   bits: 12/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5197 |    5354    19216 |    1784    3547   110712    31.2 |  2.617 % |
c |      5297 |    5347    19193 |    1962    1873    50191    26.8 |  3.390 % |
c |      5449 |    5347    19193 |    2158    2025    55815    27.6 |  3.390 % |
c |      5674 |    5338    19164 |    2374    2249    60562    26.9 |  3.616 % |
c |      6011 |    5338    19164 |    2611    2586    70612    27.3 |  3.616 % |
c |      6517 |    5338    19164 |    2873    1687    31486    18.7 |  3.616 % |
c |      7276 |    5338    19164 |    3160    2446    59373    24.3 |  3.616 % |
c |      8415 |    5338    19164 |    3476    1894    50623    26.7 |  3.616 % |
c |     10124 |    5338    19164 |    3824    3603   121053    33.6 |  3.616 % |
c |     12687 |    5338    19164 |    4206    2150    64615    30.1 |  3.616 % |
c |     16531 |    5338    19164 |    4627    3832   130043    33.9 |  3.616 % |
c |     22297 |    5338    19164 |    5089    4776   215822    45.2 |  3.616 % |
c |     30948 |    5338    19164 |    5598    2892    93500    32.3 |  3.616 % |
c |     43922 |    5338    19164 |    6158    4355   160960    37.0 |  3.616 % |
c ==============================================================================
c [1mFound solution: 810[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3277   bits: 12/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     52765 |    5343    19198 |    1781    3553   114212    32.1 |  3.616 % |
c |     52867 |    5343    19198 |    1959    1879    45760    24.4 |  4.045 % |
c |     53017 |    5343    19198 |    2155    2029    50402    24.8 |  4.045 % |
c |     53242 |    5343    19198 |    2370    2254    58626    26.0 |  4.045 % |
c |     53580 |    5343    19198 |    2607    2592    69954    27.0 |  4.045 % |
c |     54088 |    5343    19198 |    2868    1699    37685    22.2 |  4.045 % |
c |     54848 |    5343    19198 |    3155    2459    64294    26.1 |  4.045 % |
c |     55989 |    5343    19198 |    3470    1936    45903    23.7 |  4.045 % |
c |     57698 |    5343    19198 |    3817    3645   113902    31.2 |  4.045 % |
c |     60260 |    5343    19198 |    4199    2149    64136    29.8 |  4.045 % |
c |     64104 |    5343    19198 |    4619    3806   152581    40.1 |  4.045 % |
c |     69871 |    5343    19198 |    5081    4792   188135    39.3 |  4.045 % |
c |     78520 |    5343    19198 |    5589    3004    99751    33.2 |  4.045 % |
c |     91494 |    5343    19198 |    6148    4440   184082    41.5 |  4.045 % |
c |    110955 |    5343    19198 |    6763    4929   193830    39.3 |  4.045 % |
c |    140147 |    5343    19198 |    7439    6312   279159    44.2 |  4.045 % |
c |    183940 |    5343    19198 |    8183    4461   158844    35.6 |  4.045 % |
c |    249624 |    5343    19198 |    9002    7504   308134    41.1 |  4.045 % |
c |    348150 |    5343    19198 |    9902    5083   196205    38.6 |  4.045 % |
c |    495939 |    5343    19198 |   10892    6558   274217    41.8 |  4.045 % |
c |    717624 |    5343    19198 |   11981    6076   279759    46.0 |  4.045 % |
c |   1050150 |    5343    19198 |   13179   10287   394591    38.4 |  4.045 % |
c |   1548938 |    5343    19198 |   14497    7990   352083    44.1 |  4.045 % |
#### 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.95 0.90 1/54 23426
Raw data (stat): 23426 (runsolver) R 23425 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421343517 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0012 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 736 0 0 0 996 1 0 0 25 0 1 0 421343517 4554752 714 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1112 714 603 41 0 1071 0
vsize: 4448
[startup+20.0016 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 842 0 0 0 1996 2 0 0 25 0 1 0 421343517 4960256 820 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1211 820 603 41 0 1170 0
vsize: 4844
[startup+30.0016 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 843 0 0 0 2995 2 0 0 25 0 1 0 421343517 4960256 821 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1211 821 603 41 0 1170 0
vsize: 4844
[startup+40.0027 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 877 0 0 0 3996 2 0 0 25 0 1 0 421343517 5095424 855 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1244 855 603 41 0 1203 0
vsize: 4976
[startup+50.0028 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 906 0 0 0 4994 2 0 0 25 0 1 0 421343517 5226496 884 4294967295 134512640 134672761 3221224576 3221223680 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1276 884 603 41 0 1235 0
vsize: 5104
[startup+60.0025 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 963 0 0 0 5994 2 0 0 25 0 1 0 421343517 5496832 941 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1342 941 603 41 0 1301 0
vsize: 5368
[startup+70.0031 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1023 0 0 0 6994 3 0 0 25 0 1 0 421343517 5636096 1001 4294967295 134512640 134672761 3221224576 3221223680 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1376 1001 603 41 0 1335 0
vsize: 5504
[startup+80.0031 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1033 0 0 0 7992 4 0 0 25 0 1 0 421343517 5771264 1011 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1409 1011 603 41 0 1368 0
vsize: 5636
[startup+90.0026 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1065 0 0 0 8992 4 0 0 25 0 1 0 421343517 5902336 1043 4294967295 134512640 134672761 3221224576 3221223744 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1441 1043 603 41 0 1400 0
vsize: 5764
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1084 0 0 0 9992 4 0 0 25 0 1 0 421343517 6033408 1062 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1473 1062 603 41 0 1432 0
vsize: 5892
[startup+110.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1108 0 0 0 10992 4 0 0 25 0 1 0 421343517 6033408 1086 4294967295 134512640 134672761 3221224576 3221223744 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1473 1086 603 41 0 1432 0
vsize: 5892
[startup+120.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1134 0 0 0 11992 4 0 0 25 0 1 0 421343517 6168576 1112 4294967295 134512640 134672761 3221224576 3221223760 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1506 1112 603 41 0 1465 0
vsize: 6024
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1138 0 0 0 12992 4 0 0 25 0 1 0 421343517 6168576 1116 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1506 1116 603 41 0 1465 0
vsize: 6024
[startup+140.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1207 0 0 0 13992 4 0 0 25 0 1 0 421343517 6438912 1185 4294967295 134512640 134672761 3221224576 3221223680 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1572 1185 603 41 0 1531 0
vsize: 6288
[startup+150.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1261 0 0 0 14992 4 0 0 25 0 1 0 421343517 6713344 1239 4294967295 134512640 134672761 3221224576 3221223680 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1639 1239 603 41 0 1598 0
vsize: 6556
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1262 0 0 0 15992 4 0 0 25 0 1 0 421343517 6713344 1240 4294967295 134512640 134672761 3221224576 3221223760 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1639 1240 603 41 0 1598 0
vsize: 6556
[startup+170.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1268 0 0 0 16992 4 0 0 25 0 1 0 421343517 6713344 1246 4294967295 134512640 134672761 3221224576 3221223712 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1639 1246 603 41 0 1598 0
vsize: 6556
[startup+180.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1272 0 0 0 17992 5 0 0 25 0 1 0 421343517 6713344 1250 4294967295 134512640 134672761 3221224576 3221223744 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1639 1250 603 41 0 1598 0
vsize: 6556
[startup+190.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1278 0 0 0 18993 5 0 0 25 0 1 0 421343517 6852608 1256 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1673 1256 603 41 0 1632 0
vsize: 6692
[startup+200.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1330 0 0 0 19993 5 0 0 25 0 1 0 421343517 6987776 1308 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1706 1308 603 41 0 1665 0
vsize: 6824
[startup+210.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1348 0 0 0 20993 5 0 0 25 0 1 0 421343517 7127040 1326 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1740 1326 603 41 0 1699 0
vsize: 6960
[startup+220.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1369 0 0 0 21993 5 0 0 25 0 1 0 421343517 7127040 1347 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1740 1347 603 41 0 1699 0
vsize: 6960
[startup+230.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1419 0 0 0 22993 5 0 0 25 0 1 0 421343517 7397376 1397 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1806 1397 603 41 0 1765 0
vsize: 7224
[startup+240.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1432 0 0 0 23993 5 0 0 25 0 1 0 421343517 7397376 1410 4294967295 134512640 134672761 3221224576 3221223680 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1806 1410 603 41 0 1765 0
vsize: 7224
[startup+250.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1471 0 0 0 24993 5 0 0 25 0 1 0 421343517 7532544 1449 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1839 1449 603 41 0 1798 0
vsize: 7356
[startup+260.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1477 0 0 0 25993 5 0 0 25 0 1 0 421343517 7680000 1455 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1875 1455 603 41 0 1834 0
vsize: 7500
[startup+270.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1477 0 0 0 26993 5 0 0 25 0 1 0 421343517 7680000 1455 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1875 1455 603 41 0 1834 0
vsize: 7500
[startup+280.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1483 0 0 0 27993 5 0 0 25 0 1 0 421343517 7680000 1461 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1875 1461 603 41 0 1834 0
vsize: 7500
[startup+290.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1486 0 0 0 28993 5 0 0 25 0 1 0 421343517 7680000 1464 4294967295 134512640 134672761 3221224576 3221223744 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1875 1464 603 41 0 1834 0
vsize: 7500
[startup+300.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1541 0 0 0 29993 6 0 0 25 0 1 0 421343517 7827456 1519 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1911 1519 603 41 0 1870 0
vsize: 7644
[startup+310.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1541 0 0 0 30993 6 0 0 25 0 1 0 421343517 7827456 1519 4294967295 134512640 134672761 3221224576 3221223712 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1911 1519 603 41 0 1870 0
vsize: 7644
[startup+320.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1551 0 0 0 31994 6 0 0 25 0 1 0 421343517 7962624 1529 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1944 1529 603 41 0 1903 0
vsize: 7776
[startup+330.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1560 0 0 0 32994 6 0 0 25 0 1 0 421343517 7962624 1538 4294967295 134512640 134672761 3221224576 3221223680 134554665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1944 1538 603 41 0 1903 0
vsize: 7776
[startup+340.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1566 0 0 0 33994 6 0 0 25 0 1 0 421343517 7962624 1544 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1944 1544 603 41 0 1903 0
vsize: 7776
[startup+350.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1622 0 0 0 34994 6 0 0 25 0 1 0 421343517 8228864 1600 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2009 1600 603 41 0 1968 0
vsize: 8036
[startup+360.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1630 0 0 0 35994 6 0 0 25 0 1 0 421343517 8228864 1608 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2009 1608 603 41 0 1968 0
vsize: 8036
[startup+370.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1634 0 0 0 36996 6 0 0 25 0 1 0 421343517 8228864 1612 4294967295 134512640 134672761 3221224576 3221223776 134557922 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2009 1612 603 41 0 1968 0
vsize: 8036
[startup+380.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1634 0 0 0 37996 6 0 0 25 0 1 0 421343517 8228864 1612 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2009 1612 603 41 0 1968 0
vsize: 8036
[startup+390.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1634 0 0 0 38996 6 0 0 25 0 1 0 421343517 8228864 1612 4294967295 134512640 134672761 3221224576 3221223744 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2009 1612 603 41 0 1968 0
vsize: 8036
[startup+400.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1634 0 0 0 39996 6 0 0 25 0 1 0 421343517 8228864 1612 4294967295 134512640 134672761 3221224576 3221223728 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2009 1612 603 41 0 1968 0
vsize: 8036
[startup+410.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1647 0 0 0 40996 6 0 0 25 0 1 0 421343517 8364032 1625 4294967295 134512640 134672761 3221224576 3221223744 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2042 1625 603 41 0 2001 0
vsize: 8168
[startup+420.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1650 0 0 0 41997 6 0 0 25 0 1 0 421343517 8364032 1628 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2042 1628 603 41 0 2001 0
vsize: 8168
[startup+430.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1650 0 0 0 42997 6 0 0 25 0 1 0 421343517 8364032 1628 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2042 1628 603 41 0 2001 0
vsize: 8168
[startup+440.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1652 0 0 0 43997 6 0 0 25 0 1 0 421343517 8364032 1630 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2042 1630 603 41 0 2001 0
vsize: 8168
[startup+450.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1669 0 0 0 44997 6 0 0 25 0 1 0 421343517 8499200 1647 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2075 1647 603 41 0 2034 0
vsize: 8300
[startup+460.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1698 0 0 0 45997 6 0 0 25 0 1 0 421343517 8499200 1676 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2075 1676 603 41 0 2034 0
vsize: 8300
[startup+470.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1712 0 0 0 46997 6 0 0 25 0 1 0 421343517 8634368 1690 4294967295 134512640 134672761 3221224576 3221223680 134560335 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2108 1690 603 41 0 2067 0
vsize: 8432
[startup+480.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1713 0 0 0 47997 6 0 0 25 0 1 0 421343517 8634368 1691 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2108 1691 603 41 0 2067 0
vsize: 8432
[startup+490.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1719 0 0 0 48997 6 0 0 25 0 1 0 421343517 8634368 1697 4294967295 134512640 134672761 3221224576 3221223760 134559376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2108 1697 603 41 0 2067 0
vsize: 8432
[startup+500.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1722 0 0 0 49997 6 0 0 25 0 1 0 421343517 8634368 1700 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2108 1700 603 41 0 2067 0
vsize: 8432
[startup+510.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1722 0 0 0 50998 6 0 0 25 0 1 0 421343517 8634368 1700 4294967295 134512640 134672761 3221224576 3221223776 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2108 1700 603 41 0 2067 0
vsize: 8432
[startup+520.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1738 0 0 0 51998 6 0 0 25 0 1 0 421343517 8765440 1716 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2140 1716 603 41 0 2099 0
vsize: 8560
[startup+530.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1748 0 0 0 52998 6 0 0 25 0 1 0 421343517 8765440 1726 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2140 1726 603 41 0 2099 0
vsize: 8560
[startup+540.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1748 0 0 0 53998 6 0 0 25 0 1 0 421343517 8765440 1726 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2140 1726 603 41 0 2099 0
vsize: 8560
[startup+550.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1749 0 0 0 54998 6 0 0 25 0 1 0 421343517 8765440 1727 4294967295 134512640 134672761 3221224576 3221223744 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2140 1727 603 41 0 2099 0
vsize: 8560
[startup+560.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1752 0 0 0 55998 6 0 0 25 0 1 0 421343517 8765440 1730 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2140 1730 603 41 0 2099 0
vsize: 8560
[startup+570.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1756 0 0 0 56999 6 0 0 25 0 1 0 421343517 8765440 1734 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2140 1734 603 41 0 2099 0
vsize: 8560
[startup+580.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1759 0 0 0 57999 6 0 0 25 0 1 0 421343517 8765440 1737 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2140 1737 603 41 0 2099 0
vsize: 8560
[startup+590.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1768 0 0 0 58999 6 0 0 25 0 1 0 421343517 8908800 1746 4294967295 134512640 134672761 3221224576 3221223744 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2175 1746 603 41 0 2134 0
vsize: 8700
[startup+600.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1768 0 0 0 59999 7 0 0 25 0 1 0 421343517 8908800 1746 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2175 1746 603 41 0 2134 0
vsize: 8700
[startup+610.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1773 0 0 0 60999 7 0 0 25 0 1 0 421343517 8908800 1751 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2175 1751 603 41 0 2134 0
vsize: 8700
[startup+620.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1773 0 0 0 61999 7 0 0 25 0 1 0 421343517 8908800 1751 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2175 1751 603 41 0 2134 0
vsize: 8700
[startup+630.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1777 0 0 0 62999 7 0 0 25 0 1 0 421343517 8908800 1755 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2175 1755 603 41 0 2134 0
vsize: 8700
[startup+640.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1781 0 0 0 63999 7 0 0 25 0 1 0 421343517 8908800 1759 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2175 1759 603 41 0 2134 0
vsize: 8700
[startup+650.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1793 0 0 0 64999 7 0 0 25 0 1 0 421343517 8908800 1771 4294967295 134512640 134672761 3221224576 3221223680 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2175 1771 603 41 0 2134 0
vsize: 8700
[startup+660.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1795 0 0 0 66000 7 0 0 25 0 1 0 421343517 8908800 1773 4294967295 134512640 134672761 3221224576 3221223744 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2175 1773 603 41 0 2134 0
vsize: 8700
[startup+670.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1804 0 0 0 67000 7 0 0 25 0 1 0 421343517 9043968 1782 4294967295 134512640 134672761 3221224576 3221223760 134559280 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2208 1782 603 41 0 2167 0
vsize: 8832
[startup+680.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1806 0 0 0 67999 7 0 0 25 0 1 0 421343517 9043968 1784 4294967295 134512640 134672761 3221224576 3221223744 134561003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2208 1784 603 41 0 2167 0
vsize: 8832
[startup+690.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1828 0 0 0 68999 7 0 0 25 0 1 0 421343517 9043968 1806 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2208 1806 603 41 0 2167 0
vsize: 8832
[startup+700.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1829 0 0 0 69999 7 0 0 25 0 1 0 421343517 9043968 1807 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2208 1807 603 41 0 2167 0
vsize: 8832
[startup+710.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1879 0 0 0 71000 7 0 0 25 0 1 0 421343517 9306112 1857 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2272 1857 603 41 0 2231 0
vsize: 9088
[startup+720.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1881 0 0 0 72000 7 0 0 25 0 1 0 421343517 9306112 1859 4294967295 134512640 134672761 3221224576 3221223760 134559383 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2272 1859 603 41 0 2231 0
vsize: 9088
[startup+730.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1895 0 0 0 73000 7 0 0 25 0 1 0 421343517 9445376 1873 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2306 1873 603 41 0 2265 0
vsize: 9224
[startup+740.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1895 0 0 0 74000 7 0 0 25 0 1 0 421343517 9445376 1873 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2306 1873 603 41 0 2265 0
vsize: 9224
[startup+750.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1895 0 0 0 75000 7 0 0 25 0 1 0 421343517 9445376 1873 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2306 1873 603 41 0 2265 0
vsize: 9224
[startup+760.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1895 0 0 0 76000 7 0 0 25 0 1 0 421343517 9445376 1873 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2306 1873 603 41 0 2265 0
vsize: 9224
[startup+770.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1901 0 0 0 77000 7 0 0 25 0 1 0 421343517 9445376 1879 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2306 1879 603 41 0 2265 0
vsize: 9224
[startup+780.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1907 0 0 0 78001 7 0 0 25 0 1 0 421343517 9445376 1885 4294967295 134512640 134672761 3221224576 3221223712 134560667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2306 1885 603 41 0 2265 0
vsize: 9224
[startup+790.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1931 0 0 0 79001 7 0 0 25 0 1 0 421343517 9601024 1909 4294967295 134512640 134672761 3221224576 3221223760 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2344 1909 603 41 0 2303 0
vsize: 9376
[startup+800.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1936 0 0 0 80001 7 0 0 25 0 1 0 421343517 9601024 1914 4294967295 134512640 134672761 3221224576 3221223744 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2344 1914 603 41 0 2303 0
vsize: 9376
[startup+810.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1975 0 0 0 81001 7 0 0 25 0 1 0 421343517 9748480 1953 4294967295 134512640 134672761 3221224576 3221223680 134554907 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2380 1953 603 41 0 2339 0
vsize: 9520
[startup+820.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1975 0 0 0 82001 7 0 0 25 0 1 0 421343517 9748480 1953 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2380 1953 603 41 0 2339 0
vsize: 9520
[startup+830.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 1999 0 0 0 83001 7 0 0 25 0 1 0 421343517 9883648 1977 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2413 1977 603 41 0 2372 0
vsize: 9652
[startup+840.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 2007 0 0 0 84001 8 0 0 25 0 1 0 421343517 9883648 1985 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2413 1985 603 41 0 2372 0
vsize: 9652
[startup+850.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 2016 0 0 0 85002 8 0 0 25 0 1 0 421343517 9883648 1994 4294967295 134512640 134672761 3221224576 3221223744 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2413 1994 603 41 0 2372 0
vsize: 9652
[startup+860.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 2016 0 0 0 86002 8 0 0 25 0 1 0 421343517 9883648 1994 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2413 1994 603 41 0 2372 0
vsize: 9652
[startup+870.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 2020 0 0 0 87002 8 0 0 25 0 1 0 421343517 9883648 1998 4294967295 134512640 134672761 3221224576 3221223680 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2413 1998 603 41 0 2372 0
vsize: 9652
[startup+880.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 2020 0 0 0 88002 8 0 0 25 0 1 0 421343517 9883648 1998 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2413 1998 603 41 0 2372 0
vsize: 9652
[startup+890.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 2020 0 0 0 89002 8 0 0 25 0 1 0 421343517 9883648 1998 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2413 1998 603 41 0 2372 0
vsize: 9652
[startup+900.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 2020 0 0 0 90003 8 0 0 25 0 1 0 421343517 9883648 1998 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2413 1998 603 41 0 2372 0
vsize: 9652
[startup+910.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 2021 0 0 0 91003 8 0 0 25 0 1 0 421343517 9883648 1999 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2413 1999 603 41 0 2372 0
vsize: 9652
[startup+920.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 2021 0 0 0 92003 8 0 0 25 0 1 0 421343517 9883648 1999 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2413 1999 603 41 0 2372 0
vsize: 9652
[startup+930.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 2026 0 0 0 93003 8 0 0 25 0 1 0 421343517 10043392 2004 4294967295 134512640 134672761 3221224576 3221223760 134559041 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2452 2004 603 41 0 2411 0
vsize: 9808
[startup+940.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 2026 0 0 0 94003 8 0 0 25 0 1 0 421343517 10043392 2004 4294967295 134512640 134672761 3221224576 3221223744 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2452 2004 603 41 0 2411 0
vsize: 9808
[startup+950.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 2033 0 0 0 95004 8 0 0 25 0 1 0 421343517 10043392 2011 4294967295 134512640 134672761 3221224576 3221223744 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2452 2011 603 41 0 2411 0
vsize: 9808
[startup+960.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 2033 0 0 0 96004 8 0 0 25 0 1 0 421343517 10043392 2011 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2452 2011 603 41 0 2411 0
vsize: 9808
[startup+970.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 2033 0 0 0 97004 8 0 0 25 0 1 0 421343517 10043392 2011 4294967295 134512640 134672761 3221224576 3221223744 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2452 2011 603 41 0 2411 0
vsize: 9808
[startup+980.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 2110 0 0 0 98004 8 0 0 25 0 1 0 421343517 10313728 2088 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2518 2088 603 41 0 2477 0
vsize: 10072
[startup+990.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 2117 0 0 0 99004 8 0 0 25 0 1 0 421343517 10313728 2095 4294967295 134512640 134672761 3221224576 3221223668 1075351210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2518 2095 603 41 0 2477 0
vsize: 10072
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 2117 0 0 0 100004 8 0 0 25 0 1 0 421343517 10313728 2095 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2518 2095 603 41 0 2477 0
vsize: 10072
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 2118 0 0 0 101004 8 0 0 25 0 1 0 421343517 10313728 2096 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2518 2096 603 41 0 2477 0
vsize: 10072
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 2118 0 0 0 102005 8 0 0 25 0 1 0 421343517 10313728 2096 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2518 2096 603 41 0 2477 0
vsize: 10072
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 2118 0 0 0 103005 8 0 0 25 0 1 0 421343517 10313728 2096 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2518 2096 603 41 0 2477 0
vsize: 10072
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 2120 0 0 0 104004 8 0 0 25 0 1 0 421343517 10313728 2098 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2518 2098 603 41 0 2477 0
vsize: 10072
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 2124 0 0 0 105003 9 0 0 25 0 1 0 421343517 10313728 2102 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2518 2102 603 41 0 2477 0
vsize: 10072
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 2154 0 0 0 106003 9 0 0 25 0 1 0 421343517 10452992 2132 4294967295 134512640 134672761 3221224576 3221223744 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2552 2132 603 41 0 2511 0
vsize: 10208
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 2163 0 0 0 107003 9 0 0 25 0 1 0 421343517 10584064 2141 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2584 2141 603 41 0 2543 0
vsize: 10336
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 2190 0 0 0 108003 9 0 0 25 0 1 0 421343517 10723328 2168 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2618 2168 603 41 0 2577 0
vsize: 10472
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 2238 0 0 0 109003 9 0 0 25 0 1 0 421343517 10858496 2216 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2651 2216 603 41 0 2610 0
vsize: 10604
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 2252 0 0 0 110003 9 0 0 25 0 1 0 421343517 10858496 2230 4294967295 134512640 134672761 3221224576 3221223744 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2651 2230 603 41 0 2610 0
vsize: 10604
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 2281 0 0 0 111003 9 0 0 25 0 1 0 421343517 10997760 2259 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2685 2259 603 41 0 2644 0
vsize: 10740
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 2286 0 0 0 112003 9 0 0 25 0 1 0 421343517 10997760 2264 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2685 2264 603 41 0 2644 0
vsize: 10740
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 2293 0 0 0 113003 9 0 0 25 0 1 0 421343517 11145216 2271 4294967295 134512640 134672761 3221224576 3221223744 134560994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2721 2271 603 41 0 2680 0
vsize: 10884
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 2303 0 0 0 114004 9 0 0 25 0 1 0 421343517 11145216 2281 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2721 2281 603 41 0 2680 0
vsize: 10884
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 2309 0 0 0 115004 9 0 0 25 0 1 0 421343517 11145216 2287 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2721 2287 603 41 0 2680 0
vsize: 10884
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 2309 0 0 0 116004 9 0 0 25 0 1 0 421343517 11145216 2287 4294967295 134512640 134672761 3221224576 3221223680 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2721 2287 603 41 0 2680 0
vsize: 10884
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 2317 0 0 0 117004 9 0 0 25 0 1 0 421343517 11145216 2295 4294967295 134512640 134672761 3221224576 3221223712 134565098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2721 2295 603 41 0 2680 0
vsize: 10884
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 2328 0 0 0 118004 9 0 0 25 0 1 0 421343517 11284480 2306 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2755 2306 603 41 0 2714 0
vsize: 11020
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 2341 0 0 0 119005 9 0 0 25 0 1 0 421343517 11284480 2319 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2755 2319 603 41 0 2714 0
vsize: 11020
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23426
Raw data (stat): 23426 (minisat+) R 23425 20937 20936 0 -1 0 2341 0 0 0 120005 9 0 0 25 0 1 0 421343517 11284480 2319 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2755 2319 603 41 0 2714 0
vsize: 11020
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 23426
Raw data (stat): 23426 (minisat+) Z 23425 20937 20936 0 -1 12 2344 0 0 0 120005 10 0 0 25 0 1 0 421343517 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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.03
CPU time (s): 1200.16
CPU user time (s): 1200.05
CPU system time (s): 0.103984
CPU usage (%): 100.01
Max. virtual memory (Kb): 11020
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####