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-chnl20_21_pb.cnf.cr.opb
MD5SUM	112c693a7a90a8dc93ad23dc136d9b75
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	22
Number of bits of the biggest sum of numbers	5
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.026995
Number of variables	840
Total number of constraints	82
Number of constraints which are clauses	42
Number of constraints which are cardinality constraints (but not clauses)	40
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	20
Maximum length of a constraint	21
Trace number 5326

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc6 THE 2005-04-13 23:28:13 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3768 boxname=wulflinc6 idbench=8 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  112c693a7a90a8dc93ad23dc136d9b75  /oldhome/oroussel/tmp/wulflinc6/normalized-chnl20_21_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc6/normalized-chnl20_21_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc6/normalized-chnl20_21_pb.cnf.cr.opb
IDLAUNCH: 3768
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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.042
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:        909924 kB
Buffers:         34952 kB
Cached:          67872 kB
SwapCached:       2644 kB
Active:          51636 kB
Inactive:        56640 kB
HighTotal:      131008 kB
HighFree:        59332 kB
LowTotal:       903652 kB
LowFree:        850592 kB
SwapTotal:     2097136 kB
SwapFree:      2094492 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            10888 kB
Committed_AS:    63472 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 23:48:15 (client local time) WITH STATUS 0 IN 1200.4 SECONDS
stats: 3768 7 1200.4 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 82 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..........................................
c ---[  39]---> BDD-cost:   39
c ---[  38]---> BDD-cost:   39
c ---[  37]---> BDD-cost:   39
c ---[  36]---> BDD-cost:   39
c ---[  35]---> BDD-cost:   39
c ---[  34]---> BDD-cost:   39
c ---[  33]---> BDD-cost:   39
c ---[  32]---> BDD-cost:   39
c ---[  31]---> BDD-cost:   39
c ---[  30]---> BDD-cost:   39
c ---[  29]---> BDD-cost:   39
c ---[  28]---> BDD-cost:   39
c ---[  27]---> BDD-cost:   39
c ---[  26]---> BDD-cost:   39
c ---[  25]---> BDD-cost:   39
c ---[  24]---> BDD-cost:   39
c ---[  23]---> BDD-cost:   39
c ---[  22]---> BDD-cost:   39
c ---[  21]---> BDD-cost:   39
c ---[  20]---> BDD-cost:   39
c ---[  19]---> BDD-cost:   39
c ---[  18]---> BDD-cost:   39
c ---[  17]---> BDD-cost:   39
c ---[  16]---> BDD-cost:   39
c ---[  15]---> BDD-cost:   39
c ---[  14]---> BDD-cost:   39
c ---[  13]---> BDD-cost:   39
c ---[  12]---> BDD-cost:   39
c ---[  11]---> BDD-cost:   39
c ---[  10]---> BDD-cost:   39
c ---[   9]---> BDD-cost:   39
c ---[   8]---> BDD-cost:   39
c ---[   7]---> BDD-cost:   39
c ---[   6]---> BDD-cost:   39
c ---[   5]---> BDD-cost:   39
c ---[   4]---> BDD-cost:   39
c ---[   3]---> BDD-cost:   39
c ---[   2]---> BDD-cost:   39
c ---[   1]---> BDD-cost:   39
c ---[   0]---> BDD-cost:   39
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    3882    10840 |    1164       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2360          
c   -- var.elim.:  2000/2360          
c   -- var.elim.:  2360/2360          
c   -- var.elim.:  996/996          
c   -- var.elim.:  176/176          
c   -- subsuming                       
c   -- var.elim.:  618/618          
c   -- var.elim.:  374/374          
c   -- var.elim.:  134/134          
c   -- var.elim.:  132/132          
c   -- var.elim.:  68/68          
c   -- var.elim.:  60/60          
c   -- var.elim.:  62/62          
c   -- var.elim.:  64/64          
c   -- var.elim.:  66/66          
c   -- var.elim.:  68/68          
c   -- var.elim.:  70/70          
c   -- var.elim.:  72/72          
c   -- var.elim.:  74/74          
c   -- var.elim.:  76/76          
c   -- var.elim.:  78/78          
c   -- var.elim.:  80/80          
c   -- var.elim.:  182/182          
c   -- subsuming                       
c   -- var.elim.:  940/940          
c   -- var.elim.:  858/858          
c   -- var.elim.:  20/20          
c   -- subsuming                       
c   -- var.elim.:  260/260          
c   -- var.elim.:  146/146          
c   -- var.elim.:  20/20          
c |         0 |    3378    13096 |      --       0       --      -- |     --   | -504/2376
c |         0 |    3378    13096 |    1351       0        0     nan |  0.000 % |
c |       100 |    3378    13096 |    1486     100     7457    74.6 |  1.984 % |
c |       252 |    3378    13096 |    1634     252    18742    74.4 |  1.984 % |
c |       480 |    3378    13096 |    1798     480    40136    83.6 |  1.985 % |
c |       818 |    3378    13096 |    1978     818    73802    90.2 |  1.985 % |
c |      1325 |    3378    13096 |    2176    1325   127463    96.2 |  1.984 % |
c |      2088 |    3378    13096 |    2393    2088   231608   110.9 |  1.984 % |
c |      3231 |    3378    13096 |    2633    2196   265569   120.9 |  1.984 % |
c |      4939 |    3378    13096 |    2896    2800   332827   118.9 |  1.984 % |
c |      7502 |    3378    13096 |    3186    2922   333332   114.1 |  1.984 % |
c |     11346 |    3378    13096 |    3504    2838   329744   116.2 |  1.984 % |
c |     17113 |    3378    13096 |    3855    3001   385198   1#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.97 0.91 2/54 464
Raw data (stat): 464 (runsolver) R 463 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421689052 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+9.99988 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 1373 0 0 0 994 4 0 0 25 0 1 0 421689052 7147520 1351 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1745 1351 603 41 0 1704 0
vsize: 6980
[startup+20.0005 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 1738 0 0 0 1992 6 0 0 25 0 1 0 421689052 8716288 1716 4294967295 134512640 134672761 3221224544 3221223584 134614286 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2128 1716 603 41 0 2087 0
vsize: 8512
[startup+30.0003 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 2043 0 0 0 2992 6 0 0 25 0 1 0 421689052 9887744 2021 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2414 2021 603 41 0 2373 0
vsize: 9656
[startup+39.9991 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 2056 0 0 0 3992 6 0 0 25 0 1 0 421689052 10035200 2034 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2450 2034 603 41 0 2409 0
vsize: 9800
[startup+49.9997 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 2136 0 0 0 4993 6 0 0 25 0 1 0 421689052 10301440 2114 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2515 2114 603 41 0 2474 0
vsize: 10060
[startup+59.9998 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 2237 0 0 0 5993 6 0 0 25 0 1 0 421689052 10780672 2215 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2632 2215 603 41 0 2591 0
vsize: 10528
[startup+69.9996 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 2239 0 0 0 6993 6 0 0 25 0 1 0 421689052 10768384 2217 4294967295 134512640 134672761 3221224544 3221223648 134604374 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2629 2217 603 41 0 2588 0
vsize: 10516
[startup+80.0001 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 2271 0 0 0 7994 6 0 0 25 0 1 0 421689052 10887168 2249 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2658 2249 603 41 0 2617 0
vsize: 10632
[startup+90.0002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 2421 0 0 0 8994 6 0 0 25 0 1 0 421689052 11530240 2399 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2815 2399 603 41 0 2774 0
vsize: 11260
[startup+99.9991 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 2466 0 0 0 9994 6 0 0 25 0 1 0 421689052 11661312 2444 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2847 2444 603 41 0 2806 0
vsize: 11388
[startup+110 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 2552 0 0 0 10994 7 0 0 25 0 1 0 421689052 12054528 2530 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2943 2530 603 41 0 2902 0
vsize: 11772
[startup+120 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 2553 0 0 0 11995 7 0 0 25 0 1 0 421689052 12054528 2531 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2943 2531 603 41 0 2902 0
vsize: 11772
[startup+129.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 2733 0 0 0 12995 7 0 0 25 0 1 0 421689052 12816384 2711 4294967295 134512640 134672761 3221224544 3221223728 134615794 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3129 2711 603 41 0 3088 0
vsize: 12516
[startup+139.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 2738 0 0 0 13995 7 0 0 25 0 1 0 421689052 12816384 2716 4294967295 134512640 134672761 3221224544 3221223584 134612644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3129 2716 603 41 0 3088 0
vsize: 12516
[startup+149.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 2738 0 0 0 14995 7 0 0 25 0 1 0 421689052 12812288 2716 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3128 2716 603 41 0 3087 0
vsize: 12512
[startup+159.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 2738 0 0 0 15995 7 0 0 25 0 1 0 421689052 12808192 2716 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3127 2716 603 41 0 3086 0
vsize: 12508
[startup+169.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 2738 0 0 0 16996 7 0 0 25 0 1 0 421689052 12804096 2716 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3126 2716 603 41 0 3085 0
vsize: 12504
[startup+179.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 2739 0 0 0 17996 7 0 0 25 0 1 0 421689052 12804096 2717 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3126 2717 603 41 0 3085 0
vsize: 12504
[startup+189.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 2821 0 0 0 18996 7 0 0 25 0 1 0 421689052 13185024 2799 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3219 2799 603 41 0 3178 0
vsize: 12876
[startup+199.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 2986 0 0 0 19996 8 0 0 25 0 1 0 421689052 13840384 2964 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3379 2964 603 41 0 3338 0
vsize: 13516
[startup+209.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 3037 0 0 0 20997 8 0 0 25 0 1 0 421689052 13971456 3015 4294967295 134512640 134672761 3221224544 3221223648 134604307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3411 3015 603 41 0 3370 0
vsize: 13644
[startup+219.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 3085 0 0 0 21997 8 0 0 25 0 1 0 421689052 14233600 3063 4294967295 134512640 134672761 3221224544 3221223640 134616161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3475 3063 603 41 0 3434 0
vsize: 13900
[startup+229.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 3085 0 0 0 22997 8 0 0 25 0 1 0 421689052 14233600 3063 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3475 3063 603 41 0 3434 0
vsize: 13900
[startup+239.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 3085 0 0 0 23997 8 0 0 25 0 1 0 421689052 14233600 3063 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3475 3063 603 41 0 3434 0
vsize: 13900
[startup+249.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 3221 0 0 0 24997 8 0 0 25 0 1 0 421689052 14761984 3199 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3604 3199 603 41 0 3563 0
vsize: 14416
[startup+259.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 3221 0 0 0 25997 8 0 0 25 0 1 0 421689052 14761984 3199 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3604 3199 603 41 0 3563 0
vsize: 14416
[startup+269.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 3221 0 0 0 26998 8 0 0 25 0 1 0 421689052 14761984 3199 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3604 3199 603 41 0 3563 0
vsize: 14416
[startup+279.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 3221 0 0 0 27998 8 0 0 25 0 1 0 421689052 14761984 3199 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3604 3199 603 41 0 3563 0
vsize: 14416
[startup+289.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 3275 0 0 0 28998 9 0 0 25 0 1 0 421689052 14995456 3253 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3661 3253 603 41 0 3620 0
vsize: 14644
[startup+299.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 3640 0 0 0 29997 10 0 0 25 0 1 0 421689052 16437248 3618 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4013 3618 603 41 0 3972 0
vsize: 16052
[startup+309.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 3895 0 0 0 30996 11 0 0 25 0 1 0 421689052 17485824 3873 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4269 3873 603 41 0 4228 0
vsize: 17076
[startup+319.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 3895 0 0 0 31997 11 0 0 25 0 1 0 421689052 17293312 3828 4294967295 134512640 134672761 3221224544 3221223728 134615681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4222 3828 603 41 0 4181 0
vsize: 16888
[startup+329.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 3895 0 0 0 32997 11 0 0 25 0 1 0 421689052 17293312 3828 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4222 3828 603 41 0 4181 0
vsize: 16888
[startup+339.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 3895 0 0 0 33997 11 0 0 25 0 1 0 421689052 17293312 3828 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4222 3828 603 41 0 4181 0
vsize: 16888
[startup+349.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 3896 0 0 0 34998 11 0 0 25 0 1 0 421689052 17272832 3824 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4217 3824 603 41 0 4176 0
vsize: 16868
[startup+359.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 3896 0 0 0 35998 11 0 0 25 0 1 0 421689052 17272832 3824 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4217 3824 603 41 0 4176 0
vsize: 16868
[startup+369.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 3896 0 0 0 36998 11 0 0 25 0 1 0 421689052 17272832 3824 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4217 3824 603 41 0 4176 0
vsize: 16868
[startup+379.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 3896 0 0 0 37999 11 0 0 25 0 1 0 421689052 17272832 3824 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4217 3824 603 41 0 4176 0
vsize: 16868
[startup+389.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 3896 0 0 0 38999 11 0 0 25 0 1 0 421689052 17272832 3824 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4217 3824 603 41 0 4176 0
vsize: 16868
[startup+399.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 3896 0 0 0 39999 11 0 0 25 0 1 0 421689052 17272832 3824 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4217 3824 603 41 0 4176 0
vsize: 16868
[startup+409.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 3896 0 0 0 41000 11 0 0 25 0 1 0 421689052 17272832 3824 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4217 3824 603 41 0 4176 0
vsize: 16868
[startup+419.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 3896 0 0 0 42000 11 0 0 25 0 1 0 421689052 17272832 3824 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4217 3824 603 41 0 4176 0
vsize: 16868
[startup+429.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 3896 0 0 0 43000 11 0 0 25 0 1 0 421689052 17272832 3824 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4217 3824 603 41 0 4176 0
vsize: 16868
[startup+439.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4004 0 0 0 44000 11 0 0 25 0 1 0 421689052 17838080 3932 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4355 3932 603 41 0 4314 0
vsize: 17420
[startup+450 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4004 0 0 0 45001 11 0 0 25 0 1 0 421689052 17838080 3932 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4355 3932 603 41 0 4314 0
vsize: 17420
[startup+460 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4004 0 0 0 46001 11 0 0 25 0 1 0 421689052 17838080 3932 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4355 3932 603 41 0 4314 0
vsize: 17420
[startup+470 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4004 0 0 0 47001 11 0 0 25 0 1 0 421689052 17838080 3932 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4355 3932 603 41 0 4314 0
vsize: 17420
[startup+479.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4004 0 0 0 48002 11 0 0 25 0 1 0 421689052 17838080 3932 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4355 3932 603 41 0 4314 0
vsize: 17420
[startup+489.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4004 0 0 0 49002 11 0 0 25 0 1 0 421689052 17838080 3932 4294967295 134512640 134672761 3221224544 3221223632 134603905 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4355 3932 603 41 0 4314 0
vsize: 17420
[startup+499.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4004 0 0 0 50002 11 0 0 25 0 1 0 421689052 17838080 3932 4294967295 134512640 134672761 3221224544 3221223680 134614727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4355 3932 603 41 0 4314 0
vsize: 17420
[startup+510 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4004 0 0 0 51003 11 0 0 25 0 1 0 421689052 17838080 3932 4294967295 134512640 134672761 3221224544 3221223728 134615689 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4355 3932 603 41 0 4314 0
vsize: 17420
[startup+520 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4004 0 0 0 52003 11 0 0 25 0 1 0 421689052 17838080 3932 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4355 3932 603 41 0 4314 0
vsize: 17420
[startup+530 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4004 0 0 0 53003 11 0 0 25 0 1 0 421689052 17838080 3932 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4355 3932 603 41 0 4314 0
vsize: 17420
[startup+539.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4004 0 0 0 54004 11 0 0 25 0 1 0 421689052 17838080 3932 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4355 3932 603 41 0 4314 0
vsize: 17420
[startup+549.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4004 0 0 0 55004 11 0 0 25 0 1 0 421689052 17838080 3932 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4355 3932 603 41 0 4314 0
vsize: 17420
[startup+559.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4004 0 0 0 56004 11 0 0 25 0 1 0 421689052 17838080 3932 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4355 3932 603 41 0 4314 0
vsize: 17420
[startup+569.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4004 0 0 0 57005 11 0 0 25 0 1 0 421689052 17838080 3932 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4355 3932 603 41 0 4314 0
vsize: 17420
[startup+580 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4004 0 0 0 58005 11 0 0 25 0 1 0 421689052 17838080 3932 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4355 3932 603 41 0 4314 0
vsize: 17420
[startup+589.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4004 0 0 0 59005 11 0 0 25 0 1 0 421689052 17838080 3932 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4355 3932 603 41 0 4314 0
vsize: 17420
[startup+599.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4004 0 0 0 60006 11 0 0 25 0 1 0 421689052 17838080 3932 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4355 3932 603 41 0 4314 0
vsize: 17420
[startup+609.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4004 0 0 0 61006 11 0 0 25 0 1 0 421689052 17838080 3932 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4355 3932 603 41 0 4314 0
vsize: 17420
[startup+619.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4004 0 0 0 62006 11 0 0 25 0 1 0 421689052 17838080 3932 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4355 3932 603 41 0 4314 0
vsize: 17420
[startup+629.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4004 0 0 0 63007 11 0 0 25 0 1 0 421689052 17838080 3932 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4355 3932 603 41 0 4314 0
vsize: 17420
[startup+640 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4004 0 0 0 64007 11 0 0 25 0 1 0 421689052 17838080 3932 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4355 3932 603 41 0 4314 0
vsize: 17420
[startup+649.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4004 0 0 0 65007 11 0 0 25 0 1 0 421689052 17838080 3932 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4355 3932 603 41 0 4314 0
vsize: 17420
[startup+660 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4004 0 0 0 66008 11 0 0 25 0 1 0 421689052 17838080 3932 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4355 3932 603 41 0 4314 0
vsize: 17420
[startup+670 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4004 0 0 0 67008 11 0 0 25 0 1 0 421689052 17838080 3932 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4355 3932 603 41 0 4314 0
vsize: 17420
[startup+680 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4004 0 0 0 68008 11 0 0 25 0 1 0 421689052 17838080 3932 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4355 3932 603 41 0 4314 0
vsize: 17420
[startup+690 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4004 0 0 0 69009 11 0 0 25 0 1 0 421689052 17838080 3932 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4355 3932 603 41 0 4314 0
vsize: 17420
[startup+700 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4004 0 0 0 70009 11 0 0 25 0 1 0 421689052 17838080 3932 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4355 3932 603 41 0 4314 0
vsize: 17420
[startup+710 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4201 0 0 0 71009 12 0 0 25 0 1 0 421689052 18722816 4129 4294967295 134512640 134672761 3221224544 3221223640 134616317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4571 4129 603 41 0 4530 0
vsize: 18284
[startup+720 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4201 0 0 0 72009 12 0 0 25 0 1 0 421689052 18657280 4129 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4555 4129 603 41 0 4514 0
vsize: 18220
[startup+730 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4201 0 0 0 73010 12 0 0 25 0 1 0 421689052 18657280 4129 4294967295 134512640 134672761 3221224544 3221223600 134644260 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4555 4129 603 41 0 4514 0
vsize: 18220
[startup+740 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4201 0 0 0 74010 12 0 0 25 0 1 0 421689052 18657280 4129 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4555 4129 603 41 0 4514 0
vsize: 18220
[startup+750 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4381 0 0 0 75010 12 0 0 25 0 1 0 421689052 19398656 4309 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4736 4309 603 41 0 4695 0
vsize: 18944
[startup+760 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4502 0 0 0 76010 13 0 0 25 0 1 0 421689052 19894272 4430 4294967295 134512640 134672761 3221224544 3221223600 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4857 4430 603 41 0 4816 0
vsize: 19428
[startup+770 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4712 0 0 0 77009 13 0 0 25 0 1 0 421689052 20754432 4640 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5067 4640 603 41 0 5026 0
vsize: 20268
[startup+780 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4729 0 0 0 78010 13 0 0 25 0 1 0 421689052 20836352 4657 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5087 4657 603 41 0 5046 0
vsize: 20348
[startup+789.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4738 0 0 0 79010 13 0 0 25 0 1 0 421689052 20836352 4666 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5087 4666 603 41 0 5046 0
vsize: 20348
[startup+800 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4738 0 0 0 80010 13 0 0 25 0 1 0 421689052 20836352 4666 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5087 4666 603 41 0 5046 0
vsize: 20348
[startup+810 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4738 0 0 0 81011 13 0 0 25 0 1 0 421689052 20836352 4666 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5087 4666 603 41 0 5046 0
vsize: 20348
[startup+820 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4740 0 0 0 82011 14 0 0 25 0 1 0 421689052 20836352 4668 4294967295 134512640 134672761 3221224544 3221223680 134614656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5087 4668 603 41 0 5046 0
vsize: 20348
[startup+830 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4740 0 0 0 83011 14 0 0 25 0 1 0 421689052 20836352 4668 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5087 4668 603 41 0 5046 0
vsize: 20348
[startup+840 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4740 0 0 0 84012 14 0 0 25 0 1 0 421689052 20836352 4668 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5087 4668 603 41 0 5046 0
vsize: 20348
[startup+850 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4745 0 0 0 85012 14 0 0 25 0 1 0 421689052 20836352 4673 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5087 4673 603 41 0 5046 0
vsize: 20348
[startup+860 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4745 0 0 0 86012 14 0 0 25 0 1 0 421689052 20836352 4673 4294967295 134512640 134672761 3221224544 3221223728 134615585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5087 4673 603 41 0 5046 0
vsize: 20348
[startup+870 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4745 0 0 0 87013 14 0 0 25 0 1 0 421689052 20836352 4673 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5087 4673 603 41 0 5046 0
vsize: 20348
[startup+880 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4750 0 0 0 88013 14 0 0 25 0 1 0 421689052 20905984 4678 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5104 4678 603 41 0 5063 0
vsize: 20416
[startup+889.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4758 0 0 0 89013 14 0 0 25 0 1 0 421689052 20905984 4686 4294967295 134512640 134672761 3221224544 3221223728 134616020 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5104 4686 603 41 0 5063 0
vsize: 20416
[startup+899.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4769 0 0 0 90013 14 0 0 25 0 1 0 421689052 20992000 4697 4294967295 134512640 134672761 3221224544 3221223728 134615638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5125 4697 603 41 0 5084 0
vsize: 20500
[startup+909.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4795 0 0 0 91014 14 0 0 25 0 1 0 421689052 21094400 4723 4294967295 134512640 134672761 3221224544 3221223728 134615830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5150 4723 603 41 0 5109 0
vsize: 20600
[startup+919.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4801 0 0 0 92014 14 0 0 25 0 1 0 421689052 21094400 4729 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5150 4729 603 41 0 5109 0
vsize: 20600
[startup+929.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4856 0 0 0 93014 14 0 0 25 0 1 0 421689052 21348352 4784 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5212 4784 603 41 0 5171 0
vsize: 20848
[startup+939.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4928 0 0 0 94014 14 0 0 25 0 1 0 421689052 21614592 4856 4294967295 134512640 134672761 3221224544 3221223728 134615622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5277 4856 603 41 0 5236 0
vsize: 21108
[startup+949.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4946 0 0 0 95015 14 0 0 25 0 1 0 421689052 21712896 4874 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5301 4874 603 41 0 5260 0
vsize: 21204
[startup+959.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4946 0 0 0 96015 14 0 0 25 0 1 0 421689052 21712896 4874 4294967295 134512640 134672761 3221224544 3221223584 134612797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5301 4874 603 41 0 5260 0
vsize: 21204
[startup+969.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4946 0 0 0 97015 14 0 0 25 0 1 0 421689052 21422080 4823 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5230 4823 603 41 0 5189 0
vsize: 20920
[startup+979.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4946 0 0 0 98016 14 0 0 25 0 1 0 421689052 21422080 4823 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5230 4823 603 41 0 5189 0
vsize: 20920
[startup+989.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4946 0 0 0 99016 14 0 0 25 0 1 0 421689052 21422080 4823 4294967295 134512640 134672761 3221224544 3221223640 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5230 4823 603 41 0 5189 0
vsize: 20920
[startup+999.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4946 0 0 0 100016 14 0 0 25 0 1 0 421689052 21422080 4823 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5230 4823 603 41 0 5189 0
vsize: 20920
[startup+1010 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4946 0 0 0 101017 14 0 0 25 0 1 0 421689052 21422080 4823 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5230 4823 603 41 0 5189 0
vsize: 20920
[startup+1020 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4946 0 0 0 102017 14 0 0 25 0 1 0 421689052 21422080 4823 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5230 4823 603 41 0 5189 0
vsize: 20920
[startup+1030 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4946 0 0 0 103017 14 0 0 25 0 1 0 421689052 21422080 4823 4294967295 134512640 134672761 3221224544 3221223416 1075353072 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5230 4823 603 41 0 5189 0
vsize: 20920
[startup+1040 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4947 0 0 0 104018 14 0 0 25 0 1 0 421689052 21422080 4824 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5230 4824 603 41 0 5189 0
vsize: 20920
[startup+1050 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4947 0 0 0 105018 14 0 0 25 0 1 0 421689052 21422080 4824 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5230 4824 603 41 0 5189 0
vsize: 20920
[startup+1060 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4947 0 0 0 106018 14 0 0 25 0 1 0 421689052 21422080 4824 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5230 4824 603 41 0 5189 0
vsize: 20920
[startup+1070 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4951 0 0 0 107019 14 0 0 25 0 1 0 421689052 21520384 4828 4294967295 134512640 134672761 3221224544 3221223584 134612827 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5254 4828 603 41 0 5213 0
vsize: 21016
[startup+1080 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4951 0 0 0 108019 14 0 0 25 0 1 0 421689052 21520384 4828 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5254 4828 603 41 0 5213 0
vsize: 21016
[startup+1090 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4951 0 0 0 109019 14 0 0 25 0 1 0 421689052 21520384 4828 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5254 4828 603 41 0 5213 0
vsize: 21016
[startup+1100 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4951 0 0 0 110020 14 0 0 25 0 1 0 421689052 21520384 4828 4294967295 134512640 134672761 3221224544 3221223728 134615926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5254 4828 603 41 0 5213 0
vsize: 21016
[startup+1110 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4951 0 0 0 111020 14 0 0 25 0 1 0 421689052 21520384 4828 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5254 4828 603 41 0 5213 0
vsize: 21016
[startup+1120 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 4951 0 0 0 112021 14 0 0 25 0 1 0 421689052 21520384 4828 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5254 4828 603 41 0 5213 0
vsize: 21016
[startup+1130 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 5114 0 0 0 113020 15 0 0 25 0 1 0 421689052 22175744 4991 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5414 4991 603 41 0 5373 0
vsize: 21656
[startup+1140 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 5230 0 0 0 114021 15 0 0 25 0 1 0 421689052 22679552 5107 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5537 5107 603 41 0 5496 0
vsize: 22148
[startup+1150 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 5365 0 0 0 115021 15 0 0 25 0 1 0 421689052 23175168 5242 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5658 5242 603 41 0 5617 0
vsize: 22632
[startup+1160 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 5407 0 0 0 116021 15 0 0 25 0 1 0 421689052 23400448 5284 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5713 5284 603 41 0 5672 0
vsize: 22852
[startup+1170 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 5407 0 0 0 117021 15 0 0 25 0 1 0 421689052 23343104 5283 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5699 5283 603 41 0 5658 0
vsize: 22796
[startup+1180 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 5407 0 0 0 118022 15 0 0 25 0 1 0 421689052 23269376 5273 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5681 5273 603 41 0 5640 0
vsize: 22724
[startup+1190 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 5407 0 0 0 119022 15 0 0 25 0 1 0 421689052 23269376 5273 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5681 5273 603 41 0 5640 0
vsize: 22724
[startup+1200 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 464
Raw data (stat): 464 (minisat+) R 463 29653 29652 0 -1 0 5407 0 0 0 120022 15 0 0 25 0 1 0 421689052 23269376 5273 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5681 5273 603 41 0 5640 0
vsize: 22724
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 464
Raw data (stat): 464 (minisat+) Z 463 29653 29652 0 -1 12 5407 0 0 0 120022 16 0 0 25 0 1 0 421689052 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.02
CPU time (s): 1200.4
CPU user time (s): 1200.23
CPU system time (s): 0.167974
CPU usage (%): 100.032
Max. virtual memory (Kb): 22852
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####