PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/submitted/manquinho/logic-synthesis/normalized-sao2.b.opb
MD5SUM	3e273bcee52631aeea0b7b1138e7d68d
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	25
Optimality of the best value was proved	NO
Number of terms in the objective function	373
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	373
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	373
Number of bits of the biggest sum of numbers	9
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03784
Number of variables	372
Total number of constraints	779
Number of constraints which are clauses	772
Number of constraints which are cardinality constraints (but not clauses)	7
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	98
Trace number 4844

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc22 THE 2005-04-13 20:30:21 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=653 boxname=wulflinc22 idbench=73 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  3e273bcee52631aeea0b7b1138e7d68d  /oldhome/oroussel/tmp/wulflinc22/normalized-sao2.b.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc22/normalized-sao2.b.opb
IDLAUNCH: 653
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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:        870436 kB
Buffers:         30920 kB
Cached:          90344 kB
SwapCached:        524 kB
Active:          41524 kB
Inactive:        83156 kB
HighTotal:      131008 kB
HighFree:        36932 kB
LowTotal:       903652 kB
LowFree:        833504 kB
SwapTotal:     2097892 kB
SwapFree:      2097368 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            33988 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 20:50:24 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 653 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 644 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 |     644    12554 |     214       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 37[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:13602     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         1 |   15535    47286 |    5178       1       29    29.0 |  0.000 % |
c |       101 |   15487    47189 |    5695      97     2496    25.7 |  1.883 % |
c ==============================================================================
c [1mFound solution: 33[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       196 |   15413    47023 |    5137     192     7103    37.0 |  1.883 % |
c ==============================================================================
c [1mFound solution: 30[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       259 |   15441    47094 |    5147     255    10092    39.6 |  1.883 % |
c |       359 |   15441    47094 |    5661     355    13245    37.3 |  2.625 % |
c |       509 |   15441    47094 |    6227     505    18777    37.2 |  2.625 % |
c |       734 |   15441    47094 |    6850     730    31718    43.4 |  2.625 % |
c |      1074 |   15441    47094 |    7535    1070    43683    40.8 |  2.625 % |
c |      1580 |   15430    47072 |    8289    1573    77504    49.3 |  2.664 % |
c |      2339 |   15430    47072 |    9118    2332    96963    41.6 |  2.664 % |
c ==============================================================================
c [1mFound solution: 29[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2799 |   15175    46472 |    5058    2685   114769    42.7 |  2.664 % |
c |      2900 |   15175    46472 |    5563    2786   122539    44.0 |  4.394 % |
c |      3050 |   15175    46472 |    6120    2936   132076    45.0 |  4.394 % |
c |      3277 |   15175    46472 |    6732    3163   143607    45.4 |  4.394 % |
c |      3615 |   15175    46472 |    7405    3501   163393    46.7 |  4.394 % |
c |      4121 |   15159    46440 |    8145    4000   186845    46.7 |  4.443 % |
c |      4883 |   15159    46440 |    8960    4762   215959    45.4 |  4.443 % |
c |      6027 |   15159    46440 |    9856    5906   285866    48.4 |  4.443 % |
c |      7735 |   15159    46440 |   10842    7614   368092    48.3 |  4.443 % |
c |     10297 |   15159    46440 |   11926   10176   490197    48.2 |  4.443 % |
c |     14144 |   15159    46440 |   13119   14023   705041    50.3 |  4.443 % |
c |     19910 |   15159    46440 |   14431   12778   641627    50.2 |  4.443 % |
c |     28562 |   15159    46440 |   15874   13578   732753    54.0 |  4.443 % |
c ==============================================================================
c [1mFound solution: 27[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28932 |   15158    46438 |    5052   13946   750111    53.8 |  4.443 % |
c |     29032 |   15158    46438 |    5557    3587   163881    45.7 |  4.594 % |
c |     29182 |   15158    46438 |    6112    3737   169215    45.3 |  4.594 % |
c |     29407 |   15158    46438 |    6724    3962   177882    44.9 |  4.594 % |
c |     29748 |   15158    46438 |    7396    4303   184608    42.9 |  4.594 % |
c |     30255 |   15158    46438 |    8136    4810   198572    41.3 |  4.594 % |
c |     31017 |   15158    46438 |    8949    5572   239108    42.9 |  4.594 % |
c |     32156 |   15158    46438 |    9844    6711   303052    45.2 |  4.594 % |
c |     33865 |   15158    46438 |   10829    8420   394373    46.8 |  4.594 % |
c |     36428 |   15158    46438 |   11912   10983   497378    45.3 |  4.594 % |
c |     40272 |   15158    46438 |   13103    7978   332911    41.7 |  4.594 % |
c |     46038 |   15158    46438 |   14413   13744   611479    44.5 |  4.594 % |
c |     54688 |   15158    46438 |   15855   14357   644922    44.9 |  4.594 % |
c |     67662 |   15158    46438 |   17440   18249   834028    45.7 |  4.594 % |
c |     87124 |   15158    46438 |   19184   19237  1089255    56.6 |  4.594 % |
c |    116316 |   15158    46438 |   21103   16290   769799    47.3 |  4.594 % |
c |    160112 |   15158    46438 |   23213   14014   499843    35.7 |  4.594 % |
c |    225796 |   15158    46438 |   25535   18118   577512    31.9 |  4.594 % |
c |    324322 |   15158    46438 |   28088   17530   556228    31.7 |  4.594 % |
c |    472115 |   15158    46438 |   30897   17995   789226    43.9 |  4.594 % |
#### 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.94 0.90 2/54 28422
Raw data (stat): 28422 (runsolver) R 28421 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478841756 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0015 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 1637 0 0 0 994 4 0 0 25 0 1 0 478841756 8527872 1611 4294967295 134512640 134672761 3221224640 3221223808 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2082 1611 603 41 0 2041 0
vsize: 8328
[startup+20.0018 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 1963 0 0 0 1992 6 0 0 25 0 1 0 478841756 9854976 1937 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2406 1937 603 41 0 2365 0
vsize: 9624
[startup+30.0014 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 2112 0 0 0 2990 7 0 0 25 0 1 0 478841756 10526720 2086 4294967295 134512640 134672761 3221224640 3221223808 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2570 2086 603 41 0 2529 0
vsize: 10280
[startup+40.0012 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 2121 0 0 0 3989 8 0 0 25 0 1 0 478841756 10526720 2095 4294967295 134512640 134672761 3221224640 3221223808 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2570 2095 603 41 0 2529 0
vsize: 10280
[startup+50.0009 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 2121 0 0 0 4990 8 0 0 25 0 1 0 478841756 10526720 2095 4294967295 134512640 134672761 3221224640 3221223840 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2570 2095 603 41 0 2529 0
vsize: 10280
[startup+60.0016 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 2121 0 0 0 5990 8 0 0 25 0 1 0 478841756 10526720 2095 4294967295 134512640 134672761 3221224640 3221223808 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2570 2095 603 41 0 2529 0
vsize: 10280
[startup+70.0023 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 2163 0 0 0 6989 8 0 0 25 0 1 0 478841756 10657792 2137 4294967295 134512640 134672761 3221224640 3221223744 134560367 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2602 2137 603 41 0 2561 0
vsize: 10408
[startup+80.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 2209 0 0 0 7989 8 0 0 25 0 1 0 478841756 10969088 2183 4294967295 134512640 134672761 3221224640 3221223824 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2678 2183 603 41 0 2637 0
vsize: 10712
[startup+90.0021 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 2365 0 0 0 8989 9 0 0 25 0 1 0 478841756 11677696 2339 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2851 2339 603 41 0 2810 0
vsize: 11404
[startup+100.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 2381 0 0 0 9989 9 0 0 25 0 1 0 478841756 11677696 2355 4294967295 134512640 134672761 3221224640 3221223840 134557876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2851 2355 603 41 0 2810 0
vsize: 11404
[startup+110.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 2410 0 0 0 10989 9 0 0 25 0 1 0 478841756 11812864 2384 4294967295 134512640 134672761 3221224640 3221223776 134560640 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2884 2384 603 41 0 2843 0
vsize: 11536
[startup+120.003 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 2530 0 0 0 11988 10 0 0 25 0 1 0 478841756 12345344 2504 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3014 2504 603 41 0 2973 0
vsize: 12056
[startup+130.003 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 2541 0 0 0 12989 10 0 0 25 0 1 0 478841756 12345344 2515 4294967295 134512640 134672761 3221224640 3221223808 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3014 2515 603 41 0 2973 0
vsize: 12056
[startup+140.003 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 2808 0 0 0 13988 10 0 0 25 0 1 0 478841756 13414400 2782 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3275 2782 603 41 0 3234 0
vsize: 13100
[startup+150.003 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 2900 0 0 0 14988 10 0 0 25 0 1 0 478841756 13815808 2874 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3373 2874 603 41 0 3332 0
vsize: 13492
[startup+160.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 2907 0 0 0 15988 10 0 0 25 0 1 0 478841756 13815808 2881 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3373 2881 603 41 0 3332 0
vsize: 13492
[startup+170.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 2914 0 0 0 16989 10 0 0 25 0 1 0 478841756 13950976 2888 4294967295 134512640 134672761 3221224640 3221223776 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3406 2888 603 41 0 3365 0
vsize: 13624
[startup+180.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 2925 0 0 0 17989 10 0 0 25 0 1 0 478841756 13950976 2899 4294967295 134512640 134672761 3221224640 3221223808 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3406 2899 603 41 0 3365 0
vsize: 13624
[startup+190.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 2933 0 0 0 18989 10 0 0 25 0 1 0 478841756 13950976 2907 4294967295 134512640 134672761 3221224640 3221223792 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3406 2907 603 41 0 3365 0
vsize: 13624
[startup+200.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 2941 0 0 0 19989 11 0 0 25 0 1 0 478841756 13950976 2915 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3406 2915 603 41 0 3365 0
vsize: 13624
[startup+210.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 2964 0 0 0 20989 11 0 0 25 0 1 0 478841756 14114816 2938 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3446 2938 603 41 0 3405 0
vsize: 13784
[startup+220.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 2978 0 0 0 21989 11 0 0 25 0 1 0 478841756 14114816 2952 4294967295 134512640 134672761 3221224640 3221223808 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3446 2952 603 41 0 3405 0
vsize: 13784
[startup+230.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3000 0 0 0 22989 11 0 0 25 0 1 0 478841756 14278656 2974 4294967295 134512640 134672761 3221224640 3221223744 134554677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3486 2974 603 41 0 3445 0
vsize: 13944
[startup+240.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3008 0 0 0 23989 11 0 0 25 0 1 0 478841756 14278656 2982 4294967295 134512640 134672761 3221224640 3221223776 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3486 2982 603 41 0 3445 0
vsize: 13944
[startup+250.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3028 0 0 0 24989 11 0 0 25 0 1 0 478841756 14475264 3002 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3534 3002 603 41 0 3493 0
vsize: 14136
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3028 0 0 0 25990 11 0 0 25 0 1 0 478841756 14475264 3002 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3534 3002 603 41 0 3493 0
vsize: 14136
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3038 0 0 0 26990 11 0 0 25 0 1 0 478841756 14475264 3012 4294967295 134512640 134672761 3221224640 3221223808 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3534 3012 603 41 0 3493 0
vsize: 14136
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3052 0 0 0 27990 11 0 0 25 0 1 0 478841756 14639104 3026 4294967295 134512640 134672761 3221224640 3221223776 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3574 3026 603 41 0 3533 0
vsize: 14296
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3070 0 0 0 28990 11 0 0 25 0 1 0 478841756 14639104 3044 4294967295 134512640 134672761 3221224640 3221223808 134561278 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3574 3044 603 41 0 3533 0
vsize: 14296
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3072 0 0 0 29990 11 0 0 25 0 1 0 478841756 14639104 3046 4294967295 134512640 134672761 3221224640 3221223776 134560596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3574 3046 603 41 0 3533 0
vsize: 14296
[startup+310.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3072 0 0 0 30991 11 0 0 25 0 1 0 478841756 14639104 3046 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3574 3046 603 41 0 3533 0
vsize: 14296
[startup+320.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3077 0 0 0 31991 11 0 0 25 0 1 0 478841756 14802944 3051 4294967295 134512640 134672761 3221224640 3221223776 134560714 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3614 3051 603 41 0 3573 0
vsize: 14456
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3086 0 0 0 32991 11 0 0 25 0 1 0 478841756 14802944 3060 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3614 3060 603 41 0 3573 0
vsize: 14456
[startup+340.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3107 0 0 0 33991 11 0 0 25 0 1 0 478841756 14966784 3081 4294967295 134512640 134672761 3221224640 3221223804 134565156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3654 3081 603 41 0 3613 0
vsize: 14616
[startup+350.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3107 0 0 0 34991 11 0 0 25 0 1 0 478841756 14966784 3081 4294967295 134512640 134672761 3221224640 3221223808 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3654 3081 603 41 0 3613 0
vsize: 14616
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3107 0 0 0 35991 11 0 0 25 0 1 0 478841756 14966784 3081 4294967295 134512640 134672761 3221224640 3221223824 134559616 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3654 3081 603 41 0 3613 0
vsize: 14616
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3107 0 0 0 36992 11 0 0 25 0 1 0 478841756 14966784 3081 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3654 3081 603 41 0 3613 0
vsize: 14616
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3118 0 0 0 37992 11 0 0 25 0 1 0 478841756 14966784 3092 4294967295 134512640 134672761 3221224640 3221223808 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3654 3092 603 41 0 3613 0
vsize: 14616
[startup+390.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3119 0 0 0 38992 11 0 0 25 0 1 0 478841756 14966784 3093 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3654 3093 603 41 0 3613 0
vsize: 14616
[startup+400.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3120 0 0 0 39992 11 0 0 25 0 1 0 478841756 14966784 3094 4294967295 134512640 134672761 3221224640 3221223776 134560566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3654 3094 603 41 0 3613 0
vsize: 14616
[startup+410.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3124 0 0 0 40992 11 0 0 25 0 1 0 478841756 14966784 3098 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3654 3098 603 41 0 3613 0
vsize: 14616
[startup+420.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3124 0 0 0 41992 11 0 0 25 0 1 0 478841756 14966784 3098 4294967295 134512640 134672761 3221224640 3221223808 134560845 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3654 3098 603 41 0 3613 0
vsize: 14616
[startup+430.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3135 0 0 0 42992 11 0 0 25 0 1 0 478841756 14966784 3109 4294967295 134512640 134672761 3221224640 3221223776 134560716 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3654 3109 603 41 0 3613 0
vsize: 14616
[startup+440.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3135 0 0 0 43992 11 0 0 25 0 1 0 478841756 14966784 3109 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3654 3109 603 41 0 3613 0
vsize: 14616
[startup+450.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3144 0 0 0 44992 11 0 0 25 0 1 0 478841756 15163392 3118 4294967295 134512640 134672761 3221224640 3221223824 134558923 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3702 3118 603 41 0 3661 0
vsize: 14808
[startup+460.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3144 0 0 0 45993 11 0 0 25 0 1 0 478841756 15163392 3118 4294967295 134512640 134672761 3221224640 3221223840 134557885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3702 3118 603 41 0 3661 0
vsize: 14808
[startup+470.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3144 0 0 0 46993 11 0 0 25 0 1 0 478841756 15163392 3118 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3702 3118 603 41 0 3661 0
vsize: 14808
[startup+480.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3195 0 0 0 47993 12 0 0 25 0 1 0 478841756 15298560 3169 4294967295 134512640 134672761 3221224640 3221223808 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3735 3169 603 41 0 3694 0
vsize: 14940
[startup+490.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3212 0 0 0 48993 12 0 0 25 0 1 0 478841756 15470592 3186 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3777 3186 603 41 0 3736 0
vsize: 15108
[startup+500.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3213 0 0 0 49993 12 0 0 25 0 1 0 478841756 15470592 3187 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3777 3187 603 41 0 3736 0
vsize: 15108
[startup+510.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3241 0 0 0 50993 12 0 0 25 0 1 0 478841756 15470592 3215 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3777 3215 603 41 0 3736 0
vsize: 15108
[startup+520.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3242 0 0 0 51993 12 0 0 25 0 1 0 478841756 15470592 3216 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3777 3216 603 41 0 3736 0
vsize: 15108
[startup+530.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3252 0 0 0 52994 12 0 0 25 0 1 0 478841756 15630336 3226 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3816 3226 603 41 0 3775 0
vsize: 15264
[startup+540.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3252 0 0 0 53994 12 0 0 25 0 1 0 478841756 15630336 3226 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3816 3226 603 41 0 3775 0
vsize: 15264
[startup+550.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3253 0 0 0 54994 12 0 0 25 0 1 0 478841756 15630336 3227 4294967295 134512640 134672761 3221224640 3221223824 134558654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3816 3227 603 41 0 3775 0
vsize: 15264
[startup+560.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3253 0 0 0 55994 12 0 0 25 0 1 0 478841756 15630336 3227 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3816 3227 603 41 0 3775 0
vsize: 15264
[startup+570.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3258 0 0 0 56994 12 0 0 25 0 1 0 478841756 15630336 3232 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3816 3232 603 41 0 3775 0
vsize: 15264
[startup+580.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3278 0 0 0 57994 12 0 0 25 0 1 0 478841756 15790080 3252 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3855 3252 603 41 0 3814 0
vsize: 15420
[startup+590.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3279 0 0 0 58994 12 0 0 25 0 1 0 478841756 15790080 3253 4294967295 134512640 134672761 3221224640 3221223776 134565096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3855 3253 603 41 0 3814 0
vsize: 15420
[startup+600.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3299 0 0 0 59994 12 0 0 25 0 1 0 478841756 15790080 3273 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3855 3273 603 41 0 3814 0
vsize: 15420
[startup+610.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3300 0 0 0 60995 12 0 0 25 0 1 0 478841756 15790080 3274 4294967295 134512640 134672761 3221224640 3221223840 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3855 3274 603 41 0 3814 0
vsize: 15420
[startup+620.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3312 0 0 0 61995 12 0 0 25 0 1 0 478841756 15953920 3286 4294967295 134512640 134672761 3221224640 3221223808 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3895 3286 603 41 0 3854 0
vsize: 15580
[startup+630.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3317 0 0 0 62995 12 0 0 25 0 1 0 478841756 15953920 3291 4294967295 134512640 134672761 3221224640 3221223808 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3895 3291 603 41 0 3854 0
vsize: 15580
[startup+640.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3325 0 0 0 63995 12 0 0 25 0 1 0 478841756 15953920 3299 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3895 3299 603 41 0 3854 0
vsize: 15580
[startup+650.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3325 0 0 0 64995 12 0 0 25 0 1 0 478841756 15953920 3299 4294967295 134512640 134672761 3221224640 3221223776 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3895 3299 603 41 0 3854 0
vsize: 15580
[startup+660.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3331 0 0 0 65995 12 0 0 25 0 1 0 478841756 15953920 3305 4294967295 134512640 134672761 3221224640 3221223824 134558547 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3895 3305 603 41 0 3854 0
vsize: 15580
[startup+670.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3337 0 0 0 66995 12 0 0 25 0 1 0 478841756 15953920 3311 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3895 3311 603 41 0 3854 0
vsize: 15580
[startup+680.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3374 0 0 0 67995 12 0 0 25 0 1 0 478841756 16257024 3348 4294967295 134512640 134672761 3221224640 3221223808 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3969 3348 603 41 0 3928 0
vsize: 15876
[startup+690.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3500 0 0 0 68995 13 0 0 25 0 1 0 478841756 16670720 3474 4294967295 134512640 134672761 3221224640 3221223808 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4070 3474 603 41 0 4029 0
vsize: 16280
[startup+700.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3523 0 0 0 69995 13 0 0 25 0 1 0 478841756 16826368 3497 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4108 3497 603 41 0 4067 0
vsize: 16432
[startup+710.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3524 0 0 0 70996 13 0 0 25 0 1 0 478841756 16826368 3498 4294967295 134512640 134672761 3221224640 3221223808 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4108 3498 603 41 0 4067 0
vsize: 16432
[startup+720.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3591 0 0 0 71996 13 0 0 25 0 1 0 478841756 17096704 3565 4294967295 134512640 134672761 3221224640 3221223808 134560785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4174 3565 603 41 0 4133 0
vsize: 16696
[startup+730.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3594 0 0 0 72996 13 0 0 25 0 1 0 478841756 17096704 3568 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4174 3568 603 41 0 4133 0
vsize: 16696
[startup+740.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3607 0 0 0 73996 13 0 0 25 0 1 0 478841756 17256448 3581 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4213 3581 603 41 0 4172 0
vsize: 16852
[startup+750.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3615 0 0 0 74996 13 0 0 25 0 1 0 478841756 17256448 3589 4294967295 134512640 134672761 3221224640 3221223824 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4213 3589 603 41 0 4172 0
vsize: 16852
[startup+760.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3624 0 0 0 75996 13 0 0 25 0 1 0 478841756 17256448 3598 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4213 3598 603 41 0 4172 0
vsize: 16852
[startup+770.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3632 0 0 0 76996 13 0 0 25 0 1 0 478841756 17420288 3606 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4253 3606 603 41 0 4212 0
vsize: 17012
[startup+780.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3640 0 0 0 77997 13 0 0 25 0 1 0 478841756 17420288 3614 4294967295 134512640 134672761 3221224640 3221223776 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4253 3614 603 41 0 4212 0
vsize: 17012
[startup+790.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3643 0 0 0 78997 13 0 0 25 0 1 0 478841756 17420288 3617 4294967295 134512640 134672761 3221224640 3221223808 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4253 3617 603 41 0 4212 0
vsize: 17012
[startup+800.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3669 0 0 0 79997 13 0 0 25 0 1 0 478841756 17616896 3643 4294967295 134512640 134672761 3221224640 3221223840 134557814 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4301 3643 603 41 0 4260 0
vsize: 17204
[startup+810.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3670 0 0 0 80997 13 0 0 25 0 1 0 478841756 17616896 3644 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4301 3644 603 41 0 4260 0
vsize: 17204
[startup+820.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3670 0 0 0 81997 13 0 0 25 0 1 0 478841756 17616896 3644 4294967295 134512640 134672761 3221224640 3221223808 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4301 3644 603 41 0 4260 0
vsize: 17204
[startup+830.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3670 0 0 0 82997 13 0 0 25 0 1 0 478841756 17616896 3644 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4301 3644 603 41 0 4260 0
vsize: 17204
[startup+840.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3716 0 0 0 83997 13 0 0 25 0 1 0 478841756 17747968 3690 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4333 3690 603 41 0 4292 0
vsize: 17332
[startup+850.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3721 0 0 0 84997 14 0 0 25 0 1 0 478841756 17747968 3695 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4333 3695 603 41 0 4292 0
vsize: 17332
[startup+860.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3766 0 0 0 85997 14 0 0 25 0 1 0 478841756 18018304 3740 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4399 3740 603 41 0 4358 0
vsize: 17596
[startup+870.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3919 0 0 0 86997 14 0 0 25 0 1 0 478841756 18554880 3893 4294967295 134512640 134672761 3221224640 3221223808 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4530 3893 603 41 0 4489 0
vsize: 18120
[startup+880.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3922 0 0 0 87997 14 0 0 25 0 1 0 478841756 18554880 3896 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4530 3896 603 41 0 4489 0
vsize: 18120
[startup+890.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3942 0 0 0 88997 14 0 0 25 0 1 0 478841756 18718720 3916 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4570 3916 603 41 0 4529 0
vsize: 18280
[startup+900.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3942 0 0 0 89997 14 0 0 25 0 1 0 478841756 18718720 3916 4294967295 134512640 134672761 3221224640 3221223796 134561241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4570 3916 603 41 0 4529 0
vsize: 18280
[startup+910.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3942 0 0 0 90997 14 0 0 25 0 1 0 478841756 18718720 3916 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4570 3916 603 41 0 4529 0
vsize: 18280
[startup+920.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3944 0 0 0 91998 14 0 0 25 0 1 0 478841756 18718720 3918 4294967295 134512640 134672761 3221224640 3221223840 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4570 3918 603 41 0 4529 0
vsize: 18280
[startup+930.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 3988 0 0 0 92998 15 0 0 25 0 1 0 478841756 18853888 3962 4294967295 134512640 134672761 3221224640 3221223808 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4603 3962 603 41 0 4562 0
vsize: 18412
[startup+940.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 4001 0 0 0 93998 15 0 0 25 0 1 0 478841756 18989056 3975 4294967295 134512640 134672761 3221224640 3221223824 134558697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4636 3975 603 41 0 4595 0
vsize: 18544
[startup+950.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 4011 0 0 0 94998 15 0 0 25 0 1 0 478841756 18989056 3985 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4636 3985 603 41 0 4595 0
vsize: 18544
[startup+960.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 4028 0 0 0 95998 15 0 0 25 0 1 0 478841756 19124224 4002 4294967295 134512640 134672761 3221224640 3221223808 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4669 4002 603 41 0 4628 0
vsize: 18676
[startup+970.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 4030 0 0 0 96998 15 0 0 25 0 1 0 478841756 19124224 4004 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4669 4004 603 41 0 4628 0
vsize: 18676
[startup+980.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 4033 0 0 0 97998 15 0 0 25 0 1 0 478841756 19124224 4007 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4669 4007 603 41 0 4628 0
vsize: 18676
[startup+990.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 4044 0 0 0 98998 15 0 0 25 0 1 0 478841756 19271680 4018 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4705 4018 603 41 0 4664 0
vsize: 18820
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 4044 0 0 0 99999 15 0 0 25 0 1 0 478841756 19271680 4018 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4705 4018 603 41 0 4664 0
vsize: 18820
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 4068 0 0 0 100999 15 0 0 25 0 1 0 478841756 19271680 4042 4294967295 134512640 134672761 3221224640 3221223840 134557822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4705 4042 603 41 0 4664 0
vsize: 18820
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 4068 0 0 0 101999 15 0 0 25 0 1 0 478841756 19271680 4042 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4705 4042 603 41 0 4664 0
vsize: 18820
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 4069 0 0 0 102999 15 0 0 25 0 1 0 478841756 19271680 4043 4294967295 134512640 134672761 3221224640 3221223776 134560703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4705 4043 603 41 0 4664 0
vsize: 18820
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 4069 0 0 0 103999 15 0 0 25 0 1 0 478841756 19271680 4043 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4705 4043 603 41 0 4664 0
vsize: 18820
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 4069 0 0 0 105000 15 0 0 25 0 1 0 478841756 19271680 4043 4294967295 134512640 134672761 3221224640 3221223808 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4705 4043 603 41 0 4664 0
vsize: 18820
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 4185 0 0 0 105999 15 0 0 25 0 1 0 478841756 19832832 4159 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4842 4159 603 41 0 4801 0
vsize: 19368
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 4230 0 0 0 107000 16 0 0 25 0 1 0 478841756 20094976 4204 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4906 4204 603 41 0 4865 0
vsize: 19624
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 4232 0 0 0 108000 16 0 0 25 0 1 0 478841756 20094976 4206 4294967295 134512640 134672761 3221224640 3221223776 134560667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4906 4206 603 41 0 4865 0
vsize: 19624
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 4236 0 0 0 109000 16 0 0 25 0 1 0 478841756 20094976 4210 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4906 4210 603 41 0 4865 0
vsize: 19624
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 4258 0 0 0 110000 16 0 0 25 0 1 0 478841756 20267008 4232 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4948 4232 603 41 0 4907 0
vsize: 19792
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 4269 0 0 0 111000 16 0 0 25 0 1 0 478841756 20267008 4243 4294967295 134512640 134672761 3221224640 3221223808 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4948 4243 603 41 0 4907 0
vsize: 19792
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 4282 0 0 0 112000 16 0 0 25 0 1 0 478841756 20439040 4256 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4990 4256 603 41 0 4949 0
vsize: 19960
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 4285 0 0 0 113000 16 0 0 25 0 1 0 478841756 20439040 4259 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4990 4259 603 41 0 4949 0
vsize: 19960
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 4286 0 0 0 114001 16 0 0 25 0 1 0 478841756 20439040 4260 4294967295 134512640 134672761 3221224640 3221223808 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4990 4260 603 41 0 4949 0
vsize: 19960
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 4287 0 0 0 115001 16 0 0 25 0 1 0 478841756 20439040 4261 4294967295 134512640 134672761 3221224640 3221223776 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4990 4261 603 41 0 4949 0
vsize: 19960
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 4287 0 0 0 116001 16 0 0 25 0 1 0 478841756 20439040 4261 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4990 4261 603 41 0 4949 0
vsize: 19960
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 4287 0 0 0 117001 16 0 0 25 0 1 0 478841756 20439040 4261 4294967295 134512640 134672761 3221224640 3221223840 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4990 4261 603 41 0 4949 0
vsize: 19960
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 4287 0 0 0 118001 16 0 0 25 0 1 0 478841756 20439040 4261 4294967295 134512640 134672761 3221224640 3221223840 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4990 4261 603 41 0 4949 0
vsize: 19960
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 4292 0 0 0 119002 16 0 0 25 0 1 0 478841756 20439040 4266 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4990 4266 603 41 0 4949 0
vsize: 19960
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28422
Raw data (stat): 28422 (minisat+) R 28421 26298 26297 0 -1 0 4358 0 0 0 120002 16 0 0 25 0 1 0 478841756 20709376 4332 4294967295 134512640 134672761 3221224640 3221223824 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5056 4332 603 41 0 5015 0
vsize: 20224
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 28422
Raw data (stat): 28422 (minisat+) Z 28421 26298 26297 0 -1 12 4361 0 0 0 120002 17 0 0 25 0 1 0 478841756 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.04
CPU time (s): 1200.2
CPU user time (s): 1200.02
CPU system time (s): 0.173973
CPU usage (%): 100.013
Max. virtual memory (Kb): 20224
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####