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/aloul/FPGA_SAT05/normalized-chnl30_40_pb.cnf.cr.opb
MD5SUM	6a0000bd3257094a387dbf208b4df8cf
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	0
Biggest coefficient in the objective function	0
Number of bits for the biggest coefficient in the objective function	0
Sum of the numbers in the objective function	0
Number of bits of the sum of numbers in the objective function	0
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	41
Number of bits of the biggest sum of numbers	6
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.073987
Number of variables	2400
Total number of constraints	140
Number of constraints which are clauses	80
Number of constraints which are cardinality constraints (but not clauses)	60
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	30
Maximum length of a constraint	40
Trace number 5332

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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:        907800 kB
Buffers:         34516 kB
Cached:          72496 kB
SwapCached:        564 kB
Active:          52096 kB
Inactive:        58340 kB
HighTotal:      131008 kB
HighFree:        54600 kB
LowTotal:       903652 kB
LowFree:        853200 kB
SwapTotal:     2097136 kB
SwapFree:      2096572 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            10856 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 23:52:19 (client local time) WITH STATUS 0 IN 1200.26 SECONDS
stats: 3773 7 1200.26 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 140 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ................................................................................
c ---[  59]---> BDD-cost:   77
c ---[  58]---> BDD-cost:   77
c ---[  57]---> BDD-cost:   77
c ---[  56]---> BDD-cost:   77
c ---[  55]---> BDD-cost:   77
c ---[  54]---> BDD-cost:   77
c ---[  53]---> BDD-cost:   77
c ---[  52]---> BDD-cost:   77
c ---[  51]---> BDD-cost:   77
c ---[  50]---> BDD-cost:   77
c ---[  49]---> BDD-cost:   77
c ---[  48]---> BDD-cost:   77
c ---[  47]---> BDD-cost:   77
c ---[  46]---> BDD-cost:   77
c ---[  45]---> BDD-cost:   77
c ---[  44]---> BDD-cost:   77
c ---[  43]---> BDD-cost:   77
c ---[  42]---> BDD-cost:   77
c ---[  41]---> BDD-cost:   77
c ---[  40]---> BDD-cost:   77
c ---[  39]---> BDD-cost:   77
c ---[  38]---> BDD-cost:   77
c ---[  37]---> BDD-cost:   77
c ---[  36]---> BDD-cost:   77
c ---[  35]---> BDD-cost:   77
c ---[  34]---> BDD-cost:   77
c ---[  33]---> BDD-cost:   77
c ---[  32]---> BDD-cost:   77
c ---[  31]---> BDD-cost:   77
c ---[  30]---> BDD-cost:   77
c ---[  29]---> BDD-cost:   77
c ---[  28]---> BDD-cost:   77
c ---[  27]---> BDD-cost:   77
c ---[  26]---> BDD-cost:   77
c ---[  25]---> BDD-cost:   77
c ---[  24]---> BDD-cost:   77
c ---[  23]---> BDD-cost:   77
c ---[  22]---> BDD-cost:   77
c ---[  21]---> BDD-cost:   77
c ---[  20]---> BDD-cost:   77
c ---[  19]---> BDD-cost:   77
c ---[  18]---> BDD-cost:   77
c ---[  17]---> BDD-cost:   77
c ---[  16]---> BDD-cost:   77
c ---[  15]---> BDD-cost:   77
c ---[  14]---> BDD-cost:   77
c ---[  13]---> BDD-cost:   77
c ---[  12]---> BDD-cost:   77
c ---[  11]---> BDD-cost:   77
c ---[  10]---> BDD-cost:   77
c ---[   9]---> BDD-cost:   77
c ---[   8]---> BDD-cost:   77
c ---[   7]---> BDD-cost:   77
c ---[   6]---> BDD-cost:   77
c ---[   5]---> BDD-cost:   77
c ---[   4]---> BDD-cost:   77
c ---[   3]---> BDD-cost:   77
c ---[   2]---> BDD-cost:   77
c ---[   1]---> BDD-cost:   77
c ---[   0]---> BDD-cost:   77
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   11540    32220 |    3461       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/6960          
c   -- var.elim.:  2000/6960          
c   -- var.elim.:  3000/6960          
c   -- var.elim.:  4000/6960          
c   -- var.elim.:  5000/6960          
c   -- var.elim.:  6000/6960          
c   -- var.elim.:  6960/6960          
c   -- var.elim.:  1000/2656          
c   -- var.elim.:  2000/2656          
c   -- var.elim.:  2656/2656          
c   -- var.elim.:  126/126          
c   -- subsuming                       
c   -- var.elim.:  1000/1556          
c   -- var.elim.:  1556/1556          
c   -- var.elim.:  580/580          
c   -- var.elim.:  194/194          
c   -- var.elim.:  192/192          
c   -- var.elim.:  88/88          
c   -- var.elim.:  80/80          
c   -- var.elim.:  82/82          
c   -- var.elim.:  84/84          
c   -- var.elim.:  86/86          
c   -- var.elim.:  88/88          
c   -- var.elim.:  90/90          
c   -- var.elim.:  92/92          
c   -- var.elim.:  94/94          
c   -- var.elim.:  96/96          
c   -- var.elim.:  98/98          
c   -- var.elim.:  100/100          
c   -- var.elim.:  102/102          
c   -- var.elim.:  104/104          
c   -- var.elim.:  106/106          
c   -- var.elim.:  108/108          
c   -- var.elim.:  110/110          
c   -- var.elim.:  112/112          
c   -- var.elim.:  114/114          
c   -- var.elim.:  116/116          
c   -- var.elim.:  118/118          
c   -- var.elim.:  120/120          
c   -- var.elim.:  122/122          
c   -- var.elim.:  124/124         #### 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.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (runsolver) R 1291 30854 30853 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421713968 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 3397 0 0 0 989 9 0 0 25 0 1 0 421713968 15396864 3343 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3759 3343 603 41 0 3718 0
vsize: 15036
[startup+20.0014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 4373 0 0 0 1985 13 0 0 25 0 1 0 421713968 19501056 4319 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4761 4319 603 41 0 4720 0
vsize: 19044
[startup+30.0012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 5325 0 0 0 2983 15 0 0 25 0 1 0 421713968 23318528 5271 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5693 5271 603 41 0 5652 0
vsize: 22772
[startup+40.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 6045 0 0 0 3983 16 0 0 25 0 1 0 421713968 26357760 5991 4294967295 134512640 134672761 3221224544 3221223504 134645354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6435 5991 603 41 0 6394 0
vsize: 25740
[startup+50.0027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 6045 0 0 0 4983 16 0 0 25 0 1 0 421713968 26292224 5991 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6419 5991 603 41 0 6378 0
vsize: 25676
[startup+60.0035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 6596 0 0 0 5982 18 0 0 25 0 1 0 421713968 28520448 6542 4294967295 134512640 134672761 3221224544 3221223584 134613118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6963 6542 603 41 0 6922 0
vsize: 27852
[startup+70.0043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 6747 0 0 0 6982 18 0 0 25 0 1 0 421713968 29163520 6693 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7120 6693 603 41 0 7079 0
vsize: 28480
[startup+80.004 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 6975 0 0 0 7981 18 0 0 25 0 1 0 421713968 30085120 6921 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7345 6921 603 41 0 7304 0
vsize: 29380
[startup+90.0048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 7324 0 0 0 8981 19 0 0 25 0 1 0 421713968 31576064 7270 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7709 7270 603 41 0 7668 0
vsize: 30836
[startup+100.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 7324 0 0 0 9981 19 0 0 25 0 1 0 421713968 31576064 7270 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7709 7270 603 41 0 7668 0
vsize: 30836
[startup+110.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 7324 0 0 0 10981 19 0 0 25 0 1 0 421713968 31576064 7270 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7709 7270 603 41 0 7668 0
vsize: 30836
[startup+120.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 7324 0 0 0 11981 19 0 0 25 0 1 0 421713968 31571968 7269 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7708 7269 603 41 0 7667 0
vsize: 30832
[startup+130.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 7325 0 0 0 12982 19 0 0 25 0 1 0 421713968 31571968 7270 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7708 7270 603 41 0 7667 0
vsize: 30832
[startup+140.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 7325 0 0 0 13982 19 0 0 25 0 1 0 421713968 31571968 7270 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7708 7270 603 41 0 7667 0
vsize: 30832
[startup+150.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 7325 0 0 0 14982 19 0 0 25 0 1 0 421713968 31571968 7270 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7708 7270 603 41 0 7667 0
vsize: 30832
[startup+160.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 7325 0 0 0 15982 19 0 0 25 0 1 0 421713968 31571968 7270 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7708 7270 603 41 0 7667 0
vsize: 30832
[startup+170.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 7325 0 0 0 16983 19 0 0 25 0 1 0 421713968 31571968 7270 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7708 7270 603 41 0 7667 0
vsize: 30832
[startup+180.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 7325 0 0 0 17983 19 0 0 25 0 1 0 421713968 31571968 7270 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7708 7270 603 41 0 7667 0
vsize: 30832
[startup+190.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 7325 0 0 0 18983 19 0 0 25 0 1 0 421713968 31571968 7270 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7708 7270 603 41 0 7667 0
vsize: 30832
[startup+200.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 7325 0 0 0 19983 19 0 0 25 0 1 0 421713968 31571968 7270 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7708 7270 603 41 0 7667 0
vsize: 30832
[startup+210.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 7325 0 0 0 20983 19 0 0 25 0 1 0 421713968 31571968 7270 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7708 7270 603 41 0 7667 0
vsize: 30832
[startup+220.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 7325 0 0 0 21984 19 0 0 25 0 1 0 421713968 31571968 7270 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7708 7270 603 41 0 7667 0
vsize: 30832
[startup+230.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 7325 0 0 0 22984 19 0 0 25 0 1 0 421713968 31571968 7270 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7708 7270 603 41 0 7667 0
vsize: 30832
[startup+240.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 7473 0 0 0 23983 19 0 0 25 0 1 0 421713968 32157696 7417 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7851 7417 603 41 0 7810 0
vsize: 31404
[startup+250.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 7686 0 0 0 24983 20 0 0 25 0 1 0 421713968 33083392 7630 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8077 7630 603 41 0 8036 0
vsize: 32308
[startup+260.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 8253 0 0 0 25981 22 0 0 25 0 1 0 421713968 35360768 8196 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8633 8196 603 41 0 8592 0
vsize: 34532
[startup+270.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 8254 0 0 0 26981 22 0 0 25 0 1 0 421713968 35360768 8197 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8633 8197 603 41 0 8592 0
vsize: 34532
[startup+280.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 8661 0 0 0 27980 23 0 0 25 0 1 0 421713968 37064704 8604 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9049 8604 603 41 0 9008 0
vsize: 36196
[startup+290.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 9314 0 0 0 28979 25 0 0 25 0 1 0 421713968 39694336 9256 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9691 9256 603 41 0 9650 0
vsize: 38764
[startup+300.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 9314 0 0 0 29979 25 0 0 25 0 1 0 421713968 39694336 9256 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9691 9256 603 41 0 9650 0
vsize: 38764
[startup+310.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 9314 0 0 0 30979 25 0 0 25 0 1 0 421713968 39694336 9256 4294967295 134512640 134672761 3221224544 3221223552 134522369 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9691 9256 603 41 0 9650 0
vsize: 38764
[startup+320.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 9315 0 0 0 31979 25 0 0 25 0 1 0 421713968 39694336 9257 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9691 9257 603 41 0 9650 0
vsize: 38764
[startup+330.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 9315 0 0 0 32979 25 0 0 25 0 1 0 421713968 39694336 9257 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9691 9257 603 41 0 9650 0
vsize: 38764
[startup+340.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 9315 0 0 0 33980 25 0 0 25 0 1 0 421713968 39694336 9257 4294967295 134512640 134672761 3221224544 3221223728 134615767 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9691 9257 603 41 0 9650 0
vsize: 38764
[startup+350.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 9315 0 0 0 34980 25 0 0 25 0 1 0 421713968 39694336 9257 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9691 9257 603 41 0 9650 0
vsize: 38764
[startup+360.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 9315 0 0 0 35980 25 0 0 25 0 1 0 421713968 39694336 9257 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9691 9257 603 41 0 9650 0
vsize: 38764
[startup+370.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 9330 0 0 0 36980 25 0 0 25 0 1 0 421713968 39751680 9271 4294967295 134512640 134672761 3221224544 3221223728 134615711 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9705 9271 603 41 0 9664 0
vsize: 38820
[startup+380.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 9330 0 0 0 37980 25 0 0 25 0 1 0 421713968 39751680 9271 4294967295 134512640 134672761 3221224544 3221223584 134612614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9705 9271 603 41 0 9664 0
vsize: 38820
[startup+390.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 9330 0 0 0 38981 25 0 0 25 0 1 0 421713968 39751680 9271 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9705 9271 603 41 0 9664 0
vsize: 38820
[startup+400.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 9753 0 0 0 39980 26 0 0 25 0 1 0 421713968 41463808 9694 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10123 9694 603 41 0 10082 0
vsize: 40492
[startup+410.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 9753 0 0 0 40980 26 0 0 25 0 1 0 421713968 41463808 9694 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10123 9694 603 41 0 10082 0
vsize: 40492
[startup+420.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 9753 0 0 0 41980 26 0 0 25 0 1 0 421713968 41463808 9694 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10123 9694 603 41 0 10082 0
vsize: 40492
[startup+430.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 9753 0 0 0 42981 26 0 0 25 0 1 0 421713968 41463808 9694 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10123 9694 603 41 0 10082 0
vsize: 40492
[startup+440.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 9753 0 0 0 43981 26 0 0 25 0 1 0 421713968 41463808 9694 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10123 9694 603 41 0 10082 0
vsize: 40492
[startup+450.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 9959 0 0 0 44981 26 0 0 25 0 1 0 421713968 42381312 9900 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10347 9900 603 41 0 10306 0
vsize: 41388
[startup+460.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 10202 0 0 0 45980 27 0 0 25 0 1 0 421713968 43335680 10142 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10580 10142 603 41 0 10539 0
vsize: 42320
[startup+470.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 10203 0 0 0 46980 27 0 0 25 0 1 0 421713968 43335680 10143 4294967295 134512640 134672761 3221224544 3221223728 134615617 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10580 10143 603 41 0 10539 0
vsize: 42320
[startup+480.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 10204 0 0 0 47981 27 0 0 25 0 1 0 421713968 43335680 10144 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10580 10144 603 41 0 10539 0
vsize: 42320
[startup+490.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 10215 0 0 0 48981 27 0 0 25 0 1 0 421713968 43499520 10155 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10620 10155 603 41 0 10579 0
vsize: 42480
[startup+500.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 10215 0 0 0 49981 27 0 0 25 0 1 0 421713968 43499520 10155 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10620 10155 603 41 0 10579 0
vsize: 42480
[startup+510.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 10722 0 0 0 50980 29 0 0 25 0 1 0 421713968 45469696 10662 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11101 10662 603 41 0 11060 0
vsize: 44404
[startup+520.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 11389 0 0 0 51978 30 0 0 25 0 1 0 421713968 48238592 11329 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11777 11329 603 41 0 11736 0
vsize: 47108
[startup+530.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 11998 0 0 0 52977 32 0 0 25 0 1 0 421713968 50741248 11938 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12388 11938 603 41 0 12347 0
vsize: 49552
[startup+540.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 11998 0 0 0 53977 32 0 0 25 0 1 0 421713968 50741248 11938 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12388 11938 603 41 0 12347 0
vsize: 49552
[startup+550.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 11998 0 0 0 54977 32 0 0 25 0 1 0 421713968 50741248 11938 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12388 11938 603 41 0 12347 0
vsize: 49552
[startup+560.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12000 0 0 0 55977 32 0 0 25 0 1 0 421713968 50741248 11940 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12388 11940 603 41 0 12347 0
vsize: 49552
[startup+570.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12002 0 0 0 56978 32 0 0 25 0 1 0 421713968 50741248 11942 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12388 11942 603 41 0 12347 0
vsize: 49552
[startup+580.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12002 0 0 0 57978 32 0 0 25 0 1 0 421713968 50741248 11942 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12388 11942 603 41 0 12347 0
vsize: 49552
[startup+590.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12007 0 0 0 58978 32 0 0 25 0 1 0 421713968 50741248 11947 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12388 11947 603 41 0 12347 0
vsize: 49552
[startup+600.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12018 0 0 0 59978 32 0 0 25 0 1 0 421713968 50937856 11958 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12436 11958 603 41 0 12395 0
vsize: 49744
[startup+610.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12019 0 0 0 60979 32 0 0 25 0 1 0 421713968 50937856 11959 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12436 11959 603 41 0 12395 0
vsize: 49744
[startup+620.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12020 0 0 0 61979 32 0 0 25 0 1 0 421713968 50937856 11960 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12436 11960 603 41 0 12395 0
vsize: 49744
[startup+630.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12166 0 0 0 62978 32 0 0 25 0 1 0 421713968 51503104 12106 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12574 12106 603 41 0 12533 0
vsize: 50296
[startup+640.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12505 0 0 0 63978 33 0 0 25 0 1 0 421713968 52867072 12444 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12907 12444 603 41 0 12866 0
vsize: 51628
[startup+650.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12506 0 0 0 64978 33 0 0 25 0 1 0 421713968 52867072 12445 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12907 12445 603 41 0 12866 0
vsize: 51628
[startup+660.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12506 0 0 0 65978 33 0 0 25 0 1 0 421713968 52867072 12445 4294967295 134512640 134672761 3221224544 3221223584 134612604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12907 12445 603 41 0 12866 0
vsize: 51628
[startup+670.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12506 0 0 0 66979 33 0 0 25 0 1 0 421713968 52867072 12445 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12907 12445 603 41 0 12866 0
vsize: 51628
[startup+680.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12506 0 0 0 67979 33 0 0 25 0 1 0 421713968 52867072 12445 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12907 12445 603 41 0 12866 0
vsize: 51628
[startup+690.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12509 0 0 0 68979 33 0 0 25 0 1 0 421713968 52867072 12448 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12907 12448 603 41 0 12866 0
vsize: 51628
[startup+700.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12520 0 0 0 69979 33 0 0 25 0 1 0 421713968 53063680 12459 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12459 603 41 0 12914 0
vsize: 51820
[startup+710.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12520 0 0 0 70980 33 0 0 25 0 1 0 421713968 53063680 12459 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12459 603 41 0 12914 0
vsize: 51820
[startup+720.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12521 0 0 0 71980 33 0 0 25 0 1 0 421713968 53063680 12460 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12460 603 41 0 12914 0
vsize: 51820
[startup+730.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12543 0 0 0 72980 33 0 0 25 0 1 0 421713968 53063680 12482 4294967295 134512640 134672761 3221224544 3221223584 134612630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12482 603 41 0 12914 0
vsize: 51820
[startup+740.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12543 0 0 0 73980 33 0 0 25 0 1 0 421713968 53063680 12482 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12482 603 41 0 12914 0
vsize: 51820
[startup+750.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12544 0 0 0 74980 33 0 0 25 0 1 0 421713968 53063680 12483 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12483 603 41 0 12914 0
vsize: 51820
[startup+760.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12544 0 0 0 75981 33 0 0 25 0 1 0 421713968 53063680 12483 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12483 603 41 0 12914 0
vsize: 51820
[startup+770.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12544 0 0 0 76981 33 0 0 25 0 1 0 421713968 53063680 12483 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12483 603 41 0 12914 0
vsize: 51820
[startup+780.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12544 0 0 0 77981 33 0 0 25 0 1 0 421713968 53063680 12483 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12483 603 41 0 12914 0
vsize: 51820
[startup+790.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12544 0 0 0 78981 33 0 0 25 0 1 0 421713968 53063680 12483 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12483 603 41 0 12914 0
vsize: 51820
[startup+800.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12544 0 0 0 79981 33 0 0 25 0 1 0 421713968 53063680 12483 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12483 603 41 0 12914 0
vsize: 51820
[startup+810.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12547 0 0 0 80981 33 0 0 25 0 1 0 421713968 53063680 12486 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12486 603 41 0 12914 0
vsize: 51820
[startup+820.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12547 0 0 0 81982 33 0 0 25 0 1 0 421713968 53063680 12486 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12486 603 41 0 12914 0
vsize: 51820
[startup+830.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12547 0 0 0 82982 33 0 0 25 0 1 0 421713968 53063680 12486 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12486 603 41 0 12914 0
vsize: 51820
[startup+840.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12547 0 0 0 83982 33 0 0 25 0 1 0 421713968 53063680 12486 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12486 603 41 0 12914 0
vsize: 51820
[startup+850.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12547 0 0 0 84982 33 0 0 25 0 1 0 421713968 53063680 12486 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12486 603 41 0 12914 0
vsize: 51820
[startup+860.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12547 0 0 0 85982 33 0 0 25 0 1 0 421713968 53063680 12486 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12486 603 41 0 12914 0
vsize: 51820
[startup+870.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12547 0 0 0 86983 33 0 0 25 0 1 0 421713968 53063680 12486 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12486 603 41 0 12914 0
vsize: 51820
[startup+880.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12547 0 0 0 87983 33 0 0 25 0 1 0 421713968 53063680 12486 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12486 603 41 0 12914 0
vsize: 51820
[startup+890.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12547 0 0 0 88983 33 0 0 25 0 1 0 421713968 53063680 12486 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12486 603 41 0 12914 0
vsize: 51820
[startup+900.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12547 0 0 0 89983 33 0 0 25 0 1 0 421713968 53063680 12486 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12486 603 41 0 12914 0
vsize: 51820
[startup+910.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12547 0 0 0 90983 33 0 0 25 0 1 0 421713968 53063680 12486 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12486 603 41 0 12914 0
vsize: 51820
[startup+920.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12547 0 0 0 91984 33 0 0 25 0 1 0 421713968 53063680 12486 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12486 603 41 0 12914 0
vsize: 51820
[startup+930.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12547 0 0 0 92984 33 0 0 25 0 1 0 421713968 53063680 12486 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12486 603 41 0 12914 0
vsize: 51820
[startup+940.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12547 0 0 0 93984 33 0 0 25 0 1 0 421713968 53063680 12486 4294967295 134512640 134672761 3221224544 3221223728 134615591 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12486 603 41 0 12914 0
vsize: 51820
[startup+950.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12547 0 0 0 94984 33 0 0 25 0 1 0 421713968 53063680 12486 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12486 603 41 0 12914 0
vsize: 51820
[startup+960.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12547 0 0 0 95984 33 0 0 25 0 1 0 421713968 53063680 12486 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12486 603 41 0 12914 0
vsize: 51820
[startup+970.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12547 0 0 0 96985 33 0 0 25 0 1 0 421713968 53063680 12486 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12486 603 41 0 12914 0
vsize: 51820
[startup+980.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12547 0 0 0 97985 33 0 0 25 0 1 0 421713968 53063680 12486 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12486 603 41 0 12914 0
vsize: 51820
[startup+990.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12547 0 0 0 98985 33 0 0 25 0 1 0 421713968 53063680 12486 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12486 603 41 0 12914 0
vsize: 51820
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12547 0 0 0 99985 33 0 0 25 0 1 0 421713968 53063680 12486 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12486 603 41 0 12914 0
vsize: 51820
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12547 0 0 0 100985 33 0 0 25 0 1 0 421713968 53063680 12486 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12486 603 41 0 12914 0
vsize: 51820
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12547 0 0 0 101985 33 0 0 25 0 1 0 421713968 53063680 12486 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12486 603 41 0 12914 0
vsize: 51820
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12547 0 0 0 102986 33 0 0 25 0 1 0 421713968 53063680 12486 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12486 603 41 0 12914 0
vsize: 51820
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12547 0 0 0 103986 33 0 0 25 0 1 0 421713968 53063680 12486 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12486 603 41 0 12914 0
vsize: 51820
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12547 0 0 0 104986 33 0 0 25 0 1 0 421713968 53063680 12486 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12486 603 41 0 12914 0
vsize: 51820
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12547 0 0 0 105986 33 0 0 25 0 1 0 421713968 53063680 12486 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12486 603 41 0 12914 0
vsize: 51820
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12547 0 0 0 106986 33 0 0 25 0 1 0 421713968 53063680 12486 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12486 603 41 0 12914 0
vsize: 51820
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12547 0 0 0 107987 33 0 0 25 0 1 0 421713968 53063680 12486 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12486 603 41 0 12914 0
vsize: 51820
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12547 0 0 0 108987 33 0 0 25 0 1 0 421713968 53063680 12486 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12486 603 41 0 12914 0
vsize: 51820
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12547 0 0 0 109987 33 0 0 25 0 1 0 421713968 53063680 12486 4294967295 134512640 134672761 3221224544 3221223728 134615681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12486 603 41 0 12914 0
vsize: 51820
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12547 0 0 0 110987 33 0 0 25 0 1 0 421713968 53063680 12486 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12486 603 41 0 12914 0
vsize: 51820
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12547 0 0 0 111987 33 0 0 25 0 1 0 421713968 53063680 12486 4294967295 134512640 134672761 3221224544 3221223728 134615788 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12486 603 41 0 12914 0
vsize: 51820
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12552 0 0 0 112987 33 0 0 25 0 1 0 421713968 53063680 12491 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12491 603 41 0 12914 0
vsize: 51820
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12821 0 0 0 113987 34 0 0 25 0 1 0 421713968 54194176 12759 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13231 12759 603 41 0 13190 0
vsize: 52924
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12821 0 0 0 114987 34 0 0 25 0 1 0 421713968 54194176 12759 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13231 12759 603 41 0 13190 0
vsize: 52924
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12821 0 0 0 115987 34 0 0 25 0 1 0 421713968 54194176 12759 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13231 12759 603 41 0 13190 0
vsize: 52924
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12821 0 0 0 116988 34 0 0 25 0 1 0 421713968 54194176 12759 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13231 12759 603 41 0 13190 0
vsize: 52924
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12821 0 0 0 117988 34 0 0 25 0 1 0 421713968 54194176 12759 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13231 12759 603 41 0 13190 0
vsize: 52924
[startup+1190.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12821 0 0 0 118988 34 0 0 25 0 1 0 421713968 54173696 12758 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13226 12758 603 41 0 13185 0
vsize: 52904
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1292
Raw data (stat): 1292 (minisat+) R 1291 30854 30853 0 -1 0 12821 0 0 0 119988 34 0 0 25 0 1 0 421713968 54173696 12758 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13226 12758 603 41 0 13185 0
vsize: 52904
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 1292
Raw data (stat): 1292 (minisat+) Z 1291 30854 30853 0 -1 12 12821 0 0 0 119988 36 0 0 25 0 1 0 421713968 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: 0
Real time (s): 1200.06
CPU time (s): 1200.26
CPU user time (s): 1199.89
CPU system time (s): 0.367944
CPU usage (%): 100.016
Max. virtual memory (Kb): 52924
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####