PB'05 competition: run trace

Some explanations

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

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

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc30 THE 2005-04-13 20:07:11 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3544 boxname=wulflinc30 idbench=160 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  fba76bbece6bbaf52b3b51d8d6e74147  /oldhome/oroussel/tmp/wulflinc30/normalized-ii32e3.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc30/normalized-ii32e3.opb /oldhome/oroussel/tmp/wulflinc30/normalized-ii32e3.opb
IDLAUNCH: 3544
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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	: 3
cpu MHz		: 451.072
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        746664 kB
Buffers:         37096 kB
Cached:         210424 kB
SwapCached:          0 kB
Active:          79128 kB
Inactive:       171184 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        746412 kB
SwapTotal:     2097892 kB
SwapFree:      2097892 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            32148 kB
Committed_AS:    63492 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 20:27:13 (client local time) WITH STATUS 10 IN 1200.18 SECONDS
stats: 3544 7 1200.18 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 5350 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 |    5350    24606 |    1783       0        0     nan |  0.000 % |
c |       100 |    5350    24606 |    1961     100     3833    38.3 |  0.034 % |
c ==============================================================================
c [1mFound solution: 312[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1312   maxlim: 348   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       168 |   14487    57226 |    4829     168     6694    39.8 |  0.034 % |
c |       269 |   14487    57226 |    5311     269    11635    43.3 |  0.303 % |
c |       419 |   14487    57226 |    5843     419    19768    47.2 |  0.303 % |
c |       646 |   14487    57226 |    6427     646    29157    45.1 |  0.303 % |
c |       983 |   14487    57226 |    7070     983    45752    46.5 |  0.303 % |
c |      1489 |   14487    57226 |    7777    1489    71532    48.0 |  0.303 % |
c |      2248 |   14487    57226 |    8554    2248   116467    51.8 |  0.303 % |
c |      3387 |   14487    57226 |    9410    3387   202359    59.7 |  0.303 % |
c |      5095 |   14487    57226 |   10351    5095   299215    58.7 |  0.303 % |
c |      7657 |   14487    57226 |   11386    7657   521108    68.1 |  0.303 % |
c |     11501 |   14487    57226 |   12525   11501   685508    59.6 |  0.303 % |
c |     17267 |   14487    57226 |   13777   10941   664188    60.7 |  0.303 % |
c |     25918 |   14487    57226 |   15155   12627   570987    45.2 |  0.303 % |
c |     38893 |   14487    57226 |   16671    8962   828655    92.5 |  0.303 % |
c |     58357 |   14487    57226 |   18338   10671  1066714   100.0 |  0.303 % |
c |     87550 |   14487    57226 |   20171   10445  1059367   101.4 |  0.303 % |
c |    131339 |   14487    57226 |   22189   10983  1007536    91.7 |  0.303 % |
c |    197023 |   14487    57226 |   24408   18064  2076677   115.0 |  0.303 % |
c |    295549 |   14487    57226 |   26848   25920  2712647   104.7 |  0.303 % |
c |    443340 |   14487    57226 |   29533   17523  2514301   143.5 |  0.303 % |
#### 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): 1.14 1.02 0.89 2/54 13830
Raw data (stat): 13830 (runsolver) R 13829 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478701894 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 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.0001 s]
Raw data (loadavg): 1.12 1.02 0.89 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 1486 0 0 0 994 4 0 0 25 0 1 0 478701894 7553024 1464 4294967295 134512640 134672761 3221224576 3221223680 134559829 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1844 1464 603 41 0 1803 0
vsize: 7376
[startup+20.0008 s]
Raw data (loadavg): 1.10 1.02 0.89 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 1560 0 0 0 1993 5 0 0 25 0 1 0 478701894 7954432 1538 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1942 1538 603 41 0 1901 0
vsize: 7768
[startup+30.0016 s]
Raw data (loadavg): 1.08 1.02 0.89 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 2121 0 0 0 2991 7 0 0 25 0 1 0 478701894 10293248 2099 4294967295 134512640 134672761 3221224576 3221223760 134559318 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2513 2099 603 41 0 2472 0
vsize: 10052
[startup+40.0024 s]
Raw data (loadavg): 1.07 1.02 0.89 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 2199 0 0 0 3991 7 0 0 25 0 1 0 478701894 10567680 2177 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2580 2177 603 41 0 2539 0
vsize: 10320
[startup+50.0032 s]
Raw data (loadavg): 1.06 1.01 0.90 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 2398 0 0 0 4990 9 0 0 25 0 1 0 478701894 11366400 2376 4294967295 134512640 134672761 3221224576 3221223680 134560248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2775 2376 603 41 0 2734 0
vsize: 11100
[startup+60.003 s]
Raw data (loadavg): 1.05 1.01 0.90 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 2665 0 0 0 5988 10 0 0 25 0 1 0 478701894 12447744 2643 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3039 2643 603 41 0 2998 0
vsize: 12156
[startup+70.004 s]
Raw data (loadavg): 1.04 1.01 0.90 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 2810 0 0 0 6988 11 0 0 25 0 1 0 478701894 13119488 2788 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3203 2788 603 41 0 3162 0
vsize: 12812
[startup+80.0046 s]
Raw data (loadavg): 1.04 1.01 0.90 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 3008 0 0 0 7986 12 0 0 25 0 1 0 478701894 13918208 2986 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3398 2986 603 41 0 3357 0
vsize: 13592
[startup+90.0053 s]
Raw data (loadavg): 1.03 1.01 0.90 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 3015 0 0 0 8986 13 0 0 25 0 1 0 478701894 13918208 2993 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3398 2993 603 41 0 3357 0
vsize: 13592
[startup+100.006 s]
Raw data (loadavg): 1.02 1.01 0.90 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 3376 0 0 0 9985 13 0 0 25 0 1 0 478701894 15405056 3354 4294967295 134512640 134672761 3221224576 3221223744 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3761 3354 603 41 0 3720 0
vsize: 15044
[startup+110.006 s]
Raw data (loadavg): 1.02 1.01 0.90 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 3378 0 0 0 10985 14 0 0 25 0 1 0 478701894 15405056 3356 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3761 3356 603 41 0 3720 0
vsize: 15044
[startup+120.007 s]
Raw data (loadavg): 1.02 1.01 0.90 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 3378 0 0 0 11984 15 0 0 25 0 1 0 478701894 15405056 3356 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3761 3356 603 41 0 3720 0
vsize: 15044
[startup+130.007 s]
Raw data (loadavg): 1.01 1.01 0.90 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 3753 0 0 0 12983 16 0 0 25 0 1 0 478701894 16883712 3731 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4122 3731 603 41 0 4081 0
vsize: 16488
[startup+140.007 s]
Raw data (loadavg): 1.01 1.01 0.90 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 3758 0 0 0 13983 16 0 0 25 0 1 0 478701894 17027072 3736 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4157 3736 603 41 0 4116 0
vsize: 16628
[startup+150.008 s]
Raw data (loadavg): 1.01 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4201 0 0 0 14981 18 0 0 25 0 1 0 478701894 18780160 4179 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4585 4179 603 41 0 4544 0
vsize: 18340
[startup+160.008 s]
Raw data (loadavg): 1.01 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4275 0 0 0 15981 18 0 0 25 0 1 0 478701894 19046400 4253 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4650 4253 603 41 0 4609 0
vsize: 18600
[startup+170.009 s]
Raw data (loadavg): 1.01 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4275 0 0 0 16981 19 0 0 25 0 1 0 478701894 19046400 4253 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4650 4253 603 41 0 4609 0
vsize: 18600
[startup+180.009 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4276 0 0 0 17980 19 0 0 25 0 1 0 478701894 19046400 4254 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4650 4254 603 41 0 4609 0
vsize: 18600
[startup+190.01 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4276 0 0 0 18980 19 0 0 25 0 1 0 478701894 19046400 4254 4294967295 134512640 134672761 3221224576 3221223680 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4650 4254 603 41 0 4609 0
vsize: 18600
[startup+200.01 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4277 0 0 0 19980 19 0 0 25 0 1 0 478701894 19046400 4255 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4650 4255 603 41 0 4609 0
vsize: 18600
[startup+210.01 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4277 0 0 0 20979 20 0 0 25 0 1 0 478701894 19046400 4255 4294967295 134512640 134672761 3221224576 3221223712 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4650 4255 603 41 0 4609 0
vsize: 18600
[startup+220.011 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4277 0 0 0 21979 20 0 0 25 0 1 0 478701894 19046400 4255 4294967295 134512640 134672761 3221224576 3221223584 134565856 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4650 4255 603 41 0 4609 0
vsize: 18600
[startup+230.01 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4277 0 0 0 22979 21 0 0 25 0 1 0 478701894 19046400 4255 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4650 4255 603 41 0 4609 0
vsize: 18600
[startup+240.011 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4277 0 0 0 23979 21 0 0 25 0 1 0 478701894 19046400 4255 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4650 4255 603 41 0 4609 0
vsize: 18600
[startup+250.011 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4277 0 0 0 24978 21 0 0 25 0 1 0 478701894 19046400 4255 4294967295 134512640 134672761 3221224576 3221223680 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4650 4255 603 41 0 4609 0
vsize: 18600
[startup+260.012 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4277 0 0 0 25978 22 0 0 25 0 1 0 478701894 19046400 4255 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4650 4255 603 41 0 4609 0
vsize: 18600
[startup+270.012 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4277 0 0 0 26978 22 0 0 25 0 1 0 478701894 19046400 4255 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4650 4255 603 41 0 4609 0
vsize: 18600
[startup+280.012 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4277 0 0 0 27978 22 0 0 25 0 1 0 478701894 19046400 4255 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4650 4255 603 41 0 4609 0
vsize: 18600
[startup+290.013 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4279 0 0 0 28978 23 0 0 25 0 1 0 478701894 19046400 4257 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4650 4257 603 41 0 4609 0
vsize: 18600
[startup+300.014 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4279 0 0 0 29978 23 0 0 25 0 1 0 478701894 19046400 4257 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4650 4257 603 41 0 4609 0
vsize: 18600
[startup+310.014 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4279 0 0 0 30978 23 0 0 25 0 1 0 478701894 19046400 4257 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4650 4257 603 41 0 4609 0
vsize: 18600
[startup+320.014 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4279 0 0 0 31978 23 0 0 25 0 1 0 478701894 19046400 4257 4294967295 134512640 134672761 3221224576 3221223680 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4650 4257 603 41 0 4609 0
vsize: 18600
[startup+330.014 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4279 0 0 0 32978 23 0 0 25 0 1 0 478701894 19046400 4257 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4650 4257 603 41 0 4609 0
vsize: 18600
[startup+340.014 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4279 0 0 0 33978 23 0 0 25 0 1 0 478701894 19046400 4257 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4650 4257 603 41 0 4609 0
vsize: 18600
[startup+350.014 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4279 0 0 0 34978 23 0 0 25 0 1 0 478701894 19046400 4257 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4650 4257 603 41 0 4609 0
vsize: 18600
[startup+360.013 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4279 0 0 0 35978 23 0 0 25 0 1 0 478701894 19046400 4257 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4650 4257 603 41 0 4609 0
vsize: 18600
[startup+370.014 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4279 0 0 0 36979 23 0 0 25 0 1 0 478701894 19046400 4257 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4650 4257 603 41 0 4609 0
vsize: 18600
[startup+380.013 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4279 0 0 0 37979 23 0 0 25 0 1 0 478701894 19046400 4257 4294967295 134512640 134672761 3221224576 3221223744 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4650 4257 603 41 0 4609 0
vsize: 18600
[startup+390.014 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4279 0 0 0 38979 23 0 0 25 0 1 0 478701894 19046400 4257 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4650 4257 603 41 0 4609 0
vsize: 18600
[startup+400.014 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4279 0 0 0 39979 23 0 0 25 0 1 0 478701894 19046400 4257 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4650 4257 603 41 0 4609 0
vsize: 18600
[startup+410.013 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4279 0 0 0 40979 23 0 0 25 0 1 0 478701894 19046400 4257 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4650 4257 603 41 0 4609 0
vsize: 18600
[startup+420.013 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4280 0 0 0 41979 23 0 0 25 0 1 0 478701894 19046400 4258 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4650 4258 603 41 0 4609 0
vsize: 18600
[startup+430.013 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4283 0 0 0 42980 23 0 0 25 0 1 0 478701894 19189760 4261 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4685 4261 603 41 0 4644 0
vsize: 18740
[startup+440.014 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4283 0 0 0 43980 23 0 0 25 0 1 0 478701894 19189760 4261 4294967295 134512640 134672761 3221224576 3221223680 134559985 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4685 4261 603 41 0 4644 0
vsize: 18740
[startup+450.013 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4283 0 0 0 44980 23 0 0 25 0 1 0 478701894 19189760 4261 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4685 4261 603 41 0 4644 0
vsize: 18740
[startup+460.014 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4284 0 0 0 45979 24 0 0 25 0 1 0 478701894 19189760 4262 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4685 4262 603 41 0 4644 0
vsize: 18740
[startup+470.014 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4284 0 0 0 46979 24 0 0 25 0 1 0 478701894 19189760 4262 4294967295 134512640 134672761 3221224576 3221223760 134559376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4685 4262 603 41 0 4644 0
vsize: 18740
[startup+480.014 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4285 0 0 0 47979 24 0 0 25 0 1 0 478701894 19189760 4263 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4685 4263 603 41 0 4644 0
vsize: 18740
[startup+490.015 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4285 0 0 0 48979 24 0 0 25 0 1 0 478701894 19189760 4263 4294967295 134512640 134672761 3221224576 3221223760 134559663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4685 4263 603 41 0 4644 0
vsize: 18740
[startup+500.016 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4625 0 0 0 49978 25 0 0 25 0 1 0 478701894 20537344 4603 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5014 4603 603 41 0 4973 0
vsize: 20056
[startup+510.015 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4833 0 0 0 50977 26 0 0 25 0 1 0 478701894 21344256 4811 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5211 4811 603 41 0 5170 0
vsize: 20844
[startup+520.015 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4836 0 0 0 51978 26 0 0 25 0 1 0 478701894 21344256 4814 4294967295 134512640 134672761 3221224576 3221223680 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5211 4814 603 41 0 5170 0
vsize: 20844
[startup+530.015 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4836 0 0 0 52978 26 0 0 25 0 1 0 478701894 21344256 4814 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5211 4814 603 41 0 5170 0
vsize: 20844
[startup+540.015 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4836 0 0 0 53978 26 0 0 25 0 1 0 478701894 21344256 4814 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5211 4814 603 41 0 5170 0
vsize: 20844
[startup+550.016 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4836 0 0 0 54978 26 0 0 25 0 1 0 478701894 21344256 4814 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5211 4814 603 41 0 5170 0
vsize: 20844
[startup+560.015 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4836 0 0 0 55978 26 0 0 25 0 1 0 478701894 21344256 4814 4294967295 134512640 134672761 3221224576 3221223760 134558918 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5211 4814 603 41 0 5170 0
vsize: 20844
[startup+570.016 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4836 0 0 0 56978 26 0 0 25 0 1 0 478701894 21344256 4814 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5211 4814 603 41 0 5170 0
vsize: 20844
[startup+580.016 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5319 0 0 0 57977 27 0 0 25 0 1 0 478701894 23355392 5297 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5702 5297 603 41 0 5661 0
vsize: 22808
[startup+590.017 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5517 0 0 0 58977 28 0 0 25 0 1 0 478701894 24162304 5495 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5899 5495 603 41 0 5858 0
vsize: 23596
[startup+600.017 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5517 0 0 0 59977 28 0 0 25 0 1 0 478701894 24162304 5495 4294967295 134512640 134672761 3221224576 3221223680 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5899 5495 603 41 0 5858 0
vsize: 23596
[startup+610.018 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5517 0 0 0 60977 28 0 0 25 0 1 0 478701894 24162304 5495 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5899 5495 603 41 0 5858 0
vsize: 23596
[startup+620.018 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5517 0 0 0 61977 28 0 0 25 0 1 0 478701894 24162304 5495 4294967295 134512640 134672761 3221224576 3221223680 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5899 5495 603 41 0 5858 0
vsize: 23596
[startup+630.018 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5517 0 0 0 62977 28 0 0 25 0 1 0 478701894 24162304 5495 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5899 5495 603 41 0 5858 0
vsize: 23596
[startup+640.019 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5517 0 0 0 63978 28 0 0 25 0 1 0 478701894 24162304 5495 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5899 5495 603 41 0 5858 0
vsize: 23596
[startup+650.019 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5655 0 0 0 64977 29 0 0 25 0 1 0 478701894 24702976 5633 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6031 5633 603 41 0 5990 0
vsize: 24124
[startup+660.018 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5655 0 0 0 65977 29 0 0 25 0 1 0 478701894 24702976 5633 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6031 5633 603 41 0 5990 0
vsize: 24124
[startup+670.019 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5655 0 0 0 66978 29 0 0 25 0 1 0 478701894 24702976 5633 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6031 5633 603 41 0 5990 0
vsize: 24124
[startup+680.019 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5655 0 0 0 67978 29 0 0 25 0 1 0 478701894 24702976 5633 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6031 5633 603 41 0 5990 0
vsize: 24124
[startup+690.019 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5694 0 0 0 68978 29 0 0 25 0 1 0 478701894 24973312 5672 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6097 5672 603 41 0 6056 0
vsize: 24388
[startup+700.019 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5694 0 0 0 69978 29 0 0 25 0 1 0 478701894 24973312 5672 4294967295 134512640 134672761 3221224576 3221223744 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6097 5672 603 41 0 6056 0
vsize: 24388
[startup+710.019 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5694 0 0 0 70978 29 0 0 25 0 1 0 478701894 24973312 5672 4294967295 134512640 134672761 3221224576 3221223680 134560174 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6097 5672 603 41 0 6056 0
vsize: 24388
[startup+720.019 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5694 0 0 0 71978 29 0 0 25 0 1 0 478701894 24973312 5672 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6097 5672 603 41 0 6056 0
vsize: 24388
[startup+730.019 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5694 0 0 0 72978 29 0 0 25 0 1 0 478701894 24973312 5672 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6097 5672 603 41 0 6056 0
vsize: 24388
[startup+740.02 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5695 0 0 0 73979 29 0 0 25 0 1 0 478701894 24973312 5673 4294967295 134512640 134672761 3221224576 3221223760 134559365 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6097 5673 603 41 0 6056 0
vsize: 24388
[startup+750.019 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5695 0 0 0 74979 29 0 0 25 0 1 0 478701894 24973312 5673 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6097 5673 603 41 0 6056 0
vsize: 24388
[startup+760.019 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5695 0 0 0 75978 29 0 0 25 0 1 0 478701894 24973312 5673 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6097 5673 603 41 0 6056 0
vsize: 24388
[startup+770.02 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5695 0 0 0 76979 29 0 0 25 0 1 0 478701894 24973312 5673 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6097 5673 603 41 0 6056 0
vsize: 24388
[startup+780.02 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5796 0 0 0 77979 29 0 0 25 0 1 0 478701894 25378816 5774 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5774 603 41 0 6155 0
vsize: 24784
[startup+790.02 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5796 0 0 0 78979 29 0 0 25 0 1 0 478701894 25378816 5774 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5774 603 41 0 6155 0
vsize: 24784
[startup+800.019 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5796 0 0 0 79979 29 0 0 25 0 1 0 478701894 25378816 5774 4294967295 134512640 134672761 3221224576 3221223760 134559417 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5774 603 41 0 6155 0
vsize: 24784
[startup+810.019 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5796 0 0 0 80979 29 0 0 25 0 1 0 478701894 25378816 5774 4294967295 134512640 134672761 3221224576 3221223728 134565212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5774 603 41 0 6155 0
vsize: 24784
[startup+820.019 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5796 0 0 0 81979 29 0 0 25 0 1 0 478701894 25378816 5774 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5774 603 41 0 6155 0
vsize: 24784
[startup+830.019 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5796 0 0 0 82979 29 0 0 25 0 1 0 478701894 25378816 5774 4294967295 134512640 134672761 3221224576 3221223680 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5774 603 41 0 6155 0
vsize: 24784
[startup+840.019 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5796 0 0 0 83980 29 0 0 25 0 1 0 478701894 25378816 5774 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5774 603 41 0 6155 0
vsize: 24784
[startup+850.019 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5796 0 0 0 84980 29 0 0 25 0 1 0 478701894 25378816 5774 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5774 603 41 0 6155 0
vsize: 24784
[startup+860.019 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5796 0 0 0 85980 29 0 0 25 0 1 0 478701894 25378816 5774 4294967295 134512640 134672761 3221224576 3221223680 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5774 603 41 0 6155 0
vsize: 24784
[startup+870.02 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5796 0 0 0 86980 29 0 0 25 0 1 0 478701894 25378816 5774 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5774 603 41 0 6155 0
vsize: 24784
[startup+880.02 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5796 0 0 0 87980 29 0 0 25 0 1 0 478701894 25378816 5774 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5774 603 41 0 6155 0
vsize: 24784
[startup+890.021 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5928 0 0 0 88980 29 0 0 25 0 1 0 478701894 25923584 5906 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6329 5906 603 41 0 6288 0
vsize: 25316
[startup+900.021 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5935 0 0 0 89981 29 0 0 25 0 1 0 478701894 25923584 5913 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6329 5913 603 41 0 6288 0
vsize: 25316
[startup+910.021 s]
Raw data (loadavg): 1.07 1.02 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5936 0 0 0 90981 29 0 0 25 0 1 0 478701894 25923584 5914 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6329 5914 603 41 0 6288 0
vsize: 25316
[startup+920.022 s]
Raw data (loadavg): 1.06 1.02 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6118 0 0 0 91980 30 0 0 25 0 1 0 478701894 26726400 6096 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6525 6096 603 41 0 6484 0
vsize: 26100
[startup+930.023 s]
Raw data (loadavg): 1.05 1.01 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6200 0 0 0 92980 31 0 0 25 0 1 0 478701894 26992640 6178 4294967295 134512640 134672761 3221224576 3221223712 134565119 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6590 6178 603 41 0 6549 0
vsize: 26360
[startup+940.023 s]
Raw data (loadavg): 1.04 1.01 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6201 0 0 0 93980 31 0 0 25 0 1 0 478701894 26992640 6179 4294967295 134512640 134672761 3221224576 3221223680 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6590 6179 603 41 0 6549 0
vsize: 26360
[startup+950.023 s]
Raw data (loadavg): 1.04 1.01 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6201 0 0 0 94980 31 0 0 25 0 1 0 478701894 26992640 6179 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6590 6179 603 41 0 6549 0
vsize: 26360
[startup+960.023 s]
Raw data (loadavg): 1.03 1.01 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6348 0 0 0 95980 31 0 0 25 0 1 0 478701894 27668480 6326 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6755 6326 603 41 0 6714 0
vsize: 27020
[startup+970.024 s]
Raw data (loadavg): 1.02 1.01 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6492 0 0 0 96980 32 0 0 25 0 1 0 478701894 28205056 6470 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6886 6470 603 41 0 6845 0
vsize: 27544
[startup+980.024 s]
Raw data (loadavg): 1.02 1.01 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6492 0 0 0 97980 32 0 0 25 0 1 0 478701894 28205056 6470 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6886 6470 603 41 0 6845 0
vsize: 27544
[startup+990.024 s]
Raw data (loadavg): 1.02 1.01 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6492 0 0 0 98980 32 0 0 25 0 1 0 478701894 28205056 6470 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6886 6470 603 41 0 6845 0
vsize: 27544
[startup+1000.02 s]
Raw data (loadavg): 1.01 1.01 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6492 0 0 0 99980 32 0 0 25 0 1 0 478701894 28205056 6470 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6886 6470 603 41 0 6845 0
vsize: 27544
[startup+1010.02 s]
Raw data (loadavg): 1.01 1.01 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6605 0 0 0 100980 32 0 0 25 0 1 0 478701894 28610560 6583 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6985 6583 603 41 0 6944 0
vsize: 27940
[startup+1020.02 s]
Raw data (loadavg): 1.01 1.01 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6605 0 0 0 101980 32 0 0 25 0 1 0 478701894 28610560 6583 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6985 6583 603 41 0 6944 0
vsize: 27940
[startup+1030.02 s]
Raw data (loadavg): 1.01 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6605 0 0 0 102980 32 0 0 25 0 1 0 478701894 28610560 6583 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6985 6583 603 41 0 6944 0
vsize: 27940
[startup+1040.03 s]
Raw data (loadavg): 1.01 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6605 0 0 0 103981 32 0 0 25 0 1 0 478701894 28610560 6583 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6985 6583 603 41 0 6944 0
vsize: 27940
[startup+1050.03 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6605 0 0 0 104981 32 0 0 25 0 1 0 478701894 28610560 6583 4294967295 134512640 134672761 3221224576 3221223680 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6985 6583 603 41 0 6944 0
vsize: 27940
[startup+1060.02 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6605 0 0 0 105981 32 0 0 25 0 1 0 478701894 28610560 6583 4294967295 134512640 134672761 3221224576 3221223744 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6985 6583 603 41 0 6944 0
vsize: 27940
[startup+1070.03 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6605 0 0 0 106981 32 0 0 25 0 1 0 478701894 28610560 6583 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6985 6583 603 41 0 6944 0
vsize: 27940
[startup+1080.02 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6605 0 0 0 107981 32 0 0 25 0 1 0 478701894 28610560 6583 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6985 6583 603 41 0 6944 0
vsize: 27940
[startup+1090.02 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6605 0 0 0 108981 32 0 0 25 0 1 0 478701894 28610560 6583 4294967295 134512640 134672761 3221224576 3221223744 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6985 6583 603 41 0 6944 0
vsize: 27940
[startup+1100.03 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6605 0 0 0 109982 32 0 0 25 0 1 0 478701894 28610560 6583 4294967295 134512640 134672761 3221224576 3221223760 134559616 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6985 6583 603 41 0 6944 0
vsize: 27940
[startup+1110.02 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6605 0 0 0 110982 32 0 0 25 0 1 0 478701894 28610560 6583 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6985 6583 603 41 0 6944 0
vsize: 27940
[startup+1120.02 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6605 0 0 0 111982 32 0 0 25 0 1 0 478701894 28610560 6583 4294967295 134512640 134672761 3221224576 3221223680 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6985 6583 603 41 0 6944 0
vsize: 27940
[startup+1130.02 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6605 0 0 0 112982 32 0 0 25 0 1 0 478701894 28610560 6583 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6985 6583 603 41 0 6944 0
vsize: 27940
[startup+1140.03 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6605 0 0 0 113982 32 0 0 25 0 1 0 478701894 28610560 6583 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6985 6583 603 41 0 6944 0
vsize: 27940
[startup+1150.03 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6605 0 0 0 114982 32 0 0 25 0 1 0 478701894 28610560 6583 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6985 6583 603 41 0 6944 0
vsize: 27940
[startup+1160.03 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6605 0 0 0 115982 32 0 0 25 0 1 0 478701894 28610560 6583 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6985 6583 603 41 0 6944 0
vsize: 27940
[startup+1170.03 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6605 0 0 0 116983 32 0 0 25 0 1 0 478701894 28610560 6583 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6985 6583 603 41 0 6944 0
vsize: 27940
[startup+1180.03 s]
Raw data (loadavg): 1.00 1.00 0.91 3/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6605 0 0 0 117983 32 0 0 25 0 1 0 478701894 28610560 6583 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6985 6583 603 41 0 6944 0
vsize: 27940
[startup+1190.03 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6605 0 0 0 118983 32 0 0 25 0 1 0 478701894 28610560 6583 4294967295 134512640 134672761 3221224576 3221223744 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6985 6583 603 41 0 6944 0
vsize: 27940
[startup+1200.03 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 13830
Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6605 0 0 0 119983 32 0 0 25 0 1 0 478701894 28610560 6583 4294967295 134512640 134672761 3221224576 3221223744 134561115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6985 6583 603 41 0 6944 0
vsize: 27940
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 1.00 1.00 0.91 1/54 13830
Raw data (stat): 13830 (minisat+) Z 13829 11931 11930 0 -1 12 6608 0 0 0 119983 34 0 0 25 0 1 0 478701894 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.18
CPU user time (s): 1199.84
CPU system time (s): 0.341948
CPU usage (%): 100.012
Max. virtual memory (Kb): 27940
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####