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-fpga35_34_sat_pb.cnf.cr.opb
MD5SUM	f49e527e8d063bcfa5508a2b00211475
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	0
Optimality of the best value was proved	NO
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	36
Number of bits of the biggest sum of numbers	6
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	9.75752
Number of variables	1785
Total number of constraints	1293
Number of constraints which are clauses	1224
Number of constraints which are cardinality constraints (but not clauses)	69
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	17
Maximum length of a constraint	35
Trace number 5400

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        841020 kB
Buffers:         34464 kB
Cached:         119188 kB
SwapCached:       2476 kB
Active:          54520 kB
Inactive:       104544 kB
HighTotal:      131008 kB
HighFree:         8708 kB
LowTotal:       903652 kB
LowFree:        832312 kB
SwapTotal:     2097892 kB
SwapFree:      2095416 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            29172 kB
Committed_AS:    63616 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 00:00:45 (client local time) WITH STATUS 0 IN 1200.26 SECONDS
stats: 3810 7 1200.26 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1293 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[  68]---> BDD-cost:   65
c ---[  67]---> BDD-cost:   65
c ---[  66]---> BDD-cost:   65
c ---[  65]---> BDD-cost:   65
c ---[  64]---> BDD-cost:   65
c ---[  63]---> BDD-cost:   65
c ---[  62]---> BDD-cost:   65
c ---[  61]---> BDD-cost:   65
c ---[  60]---> BDD-cost:   65
c ---[  59]---> BDD-cost:   65
c ---[  58]---> BDD-cost:   65
c ---[  57]---> BDD-cost:   65
c ---[  56]---> BDD-cost:   65
c ---[  55]---> BDD-cost:   65
c ---[  54]---> BDD-cost:   65
c ---[  53]---> BDD-cost:   65
c ---[  52]---> BDD-cost:   65
c ---[  51]---> BDD-cost:   65
c ---[  50]---> BDD-cost:   65
c ---[  49]---> BDD-cost:   65
c ---[  48]---> BDD-cost:   65
c ---[  47]---> BDD-cost:   65
c ---[  46]---> BDD-cost:   65
c ---[  45]---> BDD-cost:   65
c ---[  44]---> BDD-cost:   65
c ---[  43]---> BDD-cost:   65
c ---[  42]---> BDD-cost:   65
c ---[  41]---> BDD-cost:   65
c ---[  40]---> BDD-cost:   65
c ---[  39]---> BDD-cost:   65
c ---[  38]---> BDD-cost:   65
c ---[  37]---> BDD-cost:   65
c ---[  36]---> BDD-cost:   65
c ---[  35]---> BDD-cost:   65
c ---[  34]---> BDD-cost:   65
c ---[  33]---> BDD-cost:   31
c ---[  32]---> BDD-cost:   31
c ---[  31]---> BDD-cost:   31
c ---[  30]---> BDD-cost:   31
c ---[  29]---> BDD-cost:   31
c ---[  28]---> BDD-cost:   31
c ---[  27]---> BDD-cost:   31
c ---[  26]---> BDD-cost:   31
c ---[  25]---> BDD-cost:   31
c ---[  24]---> BDD-cost:   31
c ---[  23]---> BDD-cost:   31
c ---[  22]---> BDD-cost:   31
c ---[  21]---> BDD-cost:   31
c ---[  20]---> BDD-cost:   31
c ---[  19]---> BDD-cost:   31
c ---[  18]---> BDD-cost:   31
c ---[  17]---> BDD-cost:   31
c ---[  16]---> BDD-cost:   33
c ---[  15]---> BDD-cost:   33
c ---[  14]---> BDD-cost:   33
c ---[  13]---> BDD-cost:   33
c ---[  12]---> BDD-cost:   33
c ---[  11]---> BDD-cost:   33
c ---[  10]---> BDD-cost:   33
c ---[   9]---> BDD-cost:   33
c ---[   8]---> BDD-cost:   33
c ---[   7]---> BDD-cost:   33
c ---[   6]---> BDD-cost:   33
c ---[   5]---> BDD-cost:   33
c ---[   4]---> BDD-cost:   33
c ---[   3]---> BDD-cost:   33
c ---[   2]---> BDD-cost:   33
c ---[   1]---> BDD-cost:   33
c ---[   0]---> BDD-cost:   33
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    9528    44228 |    2858       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/5079          
c   -- var.elim.:  2000/5079          
c   -- var.elim.: #### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.95 0.90 2/54 27454
Raw data (stat): 27454 (runsolver) R 27453 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479990553 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.99974 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 3311 0 0 0 989 9 0 0 25 0 1 0 479990553 15204352 3277 4294967295 134512640 134672761 3221224528 3221223712 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3712 3277 603 41 0 3671 0
vsize: 14848
[startup+20.0007 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 3948 0 0 0 1987 11 0 0 25 0 1 0 479990553 17809408 3914 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4348 3914 603 41 0 4307 0
vsize: 17392
[startup+30.0013 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 4712 0 0 0 2985 14 0 0 25 0 1 0 479990553 20942848 4678 4294967295 134512640 134672761 3221224528 3221223360 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5113 4678 603 41 0 5072 0
vsize: 20452
[startup+40.0017 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 5356 0 0 0 3983 16 0 0 25 0 1 0 479990553 23576576 5322 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5756 5322 603 41 0 5715 0
vsize: 23024
[startup+50.0028 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 5696 0 0 0 4983 16 0 0 25 0 1 0 479990553 25026560 5662 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6110 5662 603 41 0 6069 0
vsize: 24440
[startup+60.0024 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 5944 0 0 0 5983 16 0 0 25 0 1 0 479990553 26030080 5910 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6355 5910 603 41 0 6314 0
vsize: 25420
[startup+70.0028 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 5944 0 0 0 6983 16 0 0 25 0 1 0 479990553 26030080 5910 4294967295 134512640 134672761 3221224528 3221223712 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6355 5910 603 41 0 6314 0
vsize: 25420
[startup+80.0028 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 5944 0 0 0 7983 16 0 0 25 0 1 0 479990553 26030080 5910 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6355 5910 603 41 0 6314 0
vsize: 25420
[startup+90.0035 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 5944 0 0 0 8983 16 0 0 25 0 1 0 479990553 26030080 5910 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6355 5910 603 41 0 6314 0
vsize: 25420
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 5944 0 0 0 9983 16 0 0 25 0 1 0 479990553 26025984 5910 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6354 5910 603 41 0 6313 0
vsize: 25416
[startup+110.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 6087 0 0 0 10983 17 0 0 25 0 1 0 479990553 26681344 6053 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6514 6053 603 41 0 6473 0
vsize: 26056
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 6621 0 0 0 11982 18 0 0 25 0 1 0 479990553 28786688 6587 4294967295 134512640 134672761 3221224528 3221223712 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7028 6587 603 41 0 6987 0
vsize: 28112
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 7086 0 0 0 12981 19 0 0 25 0 1 0 479990553 30707712 7052 4294967295 134512640 134672761 3221224528 3221223568 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7497 7052 603 41 0 7456 0
vsize: 29988
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 7086 0 0 0 13981 19 0 0 25 0 1 0 479990553 30707712 7052 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7497 7052 603 41 0 7456 0
vsize: 29988
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 7086 0 0 0 14981 19 0 0 25 0 1 0 479990553 30707712 7052 4294967295 134512640 134672761 3221224528 3221223712 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7497 7052 603 41 0 7456 0
vsize: 29988
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 7237 0 0 0 15981 20 0 0 25 0 1 0 479990553 31363072 7203 4294967295 134512640 134672761 3221224528 3221223712 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7657 7203 603 41 0 7616 0
vsize: 30628
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 7459 0 0 0 16981 20 0 0 25 0 1 0 479990553 32243712 7425 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7872 7425 603 41 0 7831 0
vsize: 31488
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 7501 0 0 0 17981 21 0 0 25 0 1 0 479990553 32464896 7467 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7926 7467 603 41 0 7885 0
vsize: 31704
[startup+190.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 7501 0 0 0 18981 21 0 0 25 0 1 0 479990553 32464896 7467 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7926 7467 603 41 0 7885 0
vsize: 31704
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 7501 0 0 0 19981 21 0 0 25 0 1 0 479990553 32464896 7467 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7926 7467 603 41 0 7885 0
vsize: 31704
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 7501 0 0 0 20981 21 0 0 25 0 1 0 479990553 32464896 7467 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7926 7467 603 41 0 7885 0
vsize: 31704
[startup+220.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 7501 0 0 0 21981 21 0 0 25 0 1 0 479990553 32464896 7467 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7926 7467 603 41 0 7885 0
vsize: 31704
[startup+230.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 7501 0 0 0 22982 21 0 0 25 0 1 0 479990553 32464896 7467 4294967295 134512640 134672761 3221224528 3221223712 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7926 7467 603 41 0 7885 0
vsize: 31704
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 7589 0 0 0 23981 21 0 0 25 0 1 0 479990553 32849920 7554 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8020 7554 603 41 0 7979 0
vsize: 32080
[startup+250.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 7589 0 0 0 24982 21 0 0 25 0 1 0 479990553 32849920 7554 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8020 7554 603 41 0 7979 0
vsize: 32080
[startup+260.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 7589 0 0 0 25982 21 0 0 25 0 1 0 479990553 32849920 7554 4294967295 134512640 134672761 3221224528 3221223712 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8020 7554 603 41 0 7979 0
vsize: 32080
[startup+270.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 7766 0 0 0 26981 22 0 0 25 0 1 0 479990553 33570816 7730 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8196 7730 603 41 0 8155 0
vsize: 32784
[startup+280.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 7766 0 0 0 27981 22 0 0 25 0 1 0 479990553 33570816 7730 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8196 7730 603 41 0 8155 0
vsize: 32784
[startup+290.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 7819 0 0 0 28981 22 0 0 25 0 1 0 479990553 33779712 7783 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8247 7783 603 41 0 8206 0
vsize: 32988
[startup+300.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 7819 0 0 0 29981 22 0 0 25 0 1 0 479990553 33779712 7783 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8247 7783 603 41 0 8206 0
vsize: 32988
[startup+310.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 8115 0 0 0 30981 23 0 0 25 0 1 0 479990553 34979840 8078 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8540 8078 603 41 0 8499 0
vsize: 34160
[startup+320.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 8115 0 0 0 31981 23 0 0 25 0 1 0 479990553 34979840 8078 4294967295 134512640 134672761 3221224528 3221223712 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8540 8078 603 41 0 8499 0
vsize: 34160
[startup+330.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 8115 0 0 0 32981 23 0 0 25 0 1 0 479990553 34979840 8078 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8540 8078 603 41 0 8499 0
vsize: 34160
[startup+340.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 8115 0 0 0 33981 23 0 0 25 0 1 0 479990553 34979840 8078 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8540 8078 603 41 0 8499 0
vsize: 34160
[startup+350.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 8115 0 0 0 34982 23 0 0 25 0 1 0 479990553 34979840 8078 4294967295 134512640 134672761 3221224528 3221223712 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8540 8078 603 41 0 8499 0
vsize: 34160
[startup+360.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 8115 0 0 0 35982 23 0 0 25 0 1 0 479990553 34979840 8078 4294967295 134512640 134672761 3221224528 3221223712 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8540 8078 603 41 0 8499 0
vsize: 34160
[startup+370.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 8115 0 0 0 36982 23 0 0 25 0 1 0 479990553 34979840 8078 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8540 8078 603 41 0 8499 0
vsize: 34160
[startup+380.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 8115 0 0 0 37982 23 0 0 25 0 1 0 479990553 34979840 8078 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8540 8078 603 41 0 8499 0
vsize: 34160
[startup+390.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 8121 0 0 0 38982 23 0 0 25 0 1 0 479990553 34979840 8084 4294967295 134512640 134672761 3221224528 3221223680 134565076 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8540 8084 603 41 0 8499 0
vsize: 34160
[startup+400.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 8173 0 0 0 39982 23 0 0 25 0 1 0 479990553 35258368 8136 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8608 8136 603 41 0 8567 0
vsize: 34432
[startup+410.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 8173 0 0 0 40982 23 0 0 25 0 1 0 479990553 35258368 8136 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8608 8136 603 41 0 8567 0
vsize: 34432
[startup+420.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 8179 0 0 0 41983 23 0 0 25 0 1 0 479990553 35258368 8142 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8608 8142 603 41 0 8567 0
vsize: 34432
[startup+430.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 8179 0 0 0 42983 23 0 0 25 0 1 0 479990553 35258368 8142 4294967295 134512640 134672761 3221224528 3221223712 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8608 8142 603 41 0 8567 0
vsize: 34432
[startup+440.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 8287 0 0 0 43983 24 0 0 25 0 1 0 479990553 35848192 8250 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8752 8250 603 41 0 8711 0
vsize: 35008
[startup+450.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 8389 0 0 0 44982 24 0 0 25 0 1 0 479990553 36200448 8352 4294967295 134512640 134672761 3221224528 3221223712 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8838 8352 603 41 0 8797 0
vsize: 35352
[startup+460.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 8389 0 0 0 45983 24 0 0 25 0 1 0 479990553 36200448 8352 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8838 8352 603 41 0 8797 0
vsize: 35352
[startup+470.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 8410 0 0 0 46983 24 0 0 25 0 1 0 479990553 36364288 8373 4294967295 134512640 134672761 3221224528 3221223568 134612797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8878 8373 603 41 0 8837 0
vsize: 35512
[startup+480.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 8430 0 0 0 47983 24 0 0 25 0 1 0 479990553 36429824 8392 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8894 8392 603 41 0 8853 0
vsize: 35576
[startup+490.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 8447 0 0 0 48983 24 0 0 25 0 1 0 479990553 36622336 8409 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8941 8409 603 41 0 8900 0
vsize: 35764
[startup+500.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 8481 0 0 0 49983 24 0 0 25 0 1 0 479990553 36818944 8443 4294967295 134512640 134672761 3221224528 3221223624 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8989 8443 603 41 0 8948 0
vsize: 35956
[startup+510.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 8481 0 0 0 50983 24 0 0 25 0 1 0 479990553 36687872 8442 4294967295 134512640 134672761 3221224528 3221223664 134614670 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8957 8442 603 41 0 8916 0
vsize: 35828
[startup+520.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 8481 0 0 0 51983 24 0 0 25 0 1 0 479990553 36687872 8442 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8957 8442 603 41 0 8916 0
vsize: 35828
[startup+530.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 8483 0 0 0 52984 24 0 0 25 0 1 0 479990553 36687872 8444 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8957 8444 603 41 0 8916 0
vsize: 35828
[startup+540.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 8483 0 0 0 53984 24 0 0 25 0 1 0 479990553 36687872 8444 4294967295 134512640 134672761 3221224528 3221223712 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8957 8444 603 41 0 8916 0
vsize: 35828
[startup+550.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 8483 0 0 0 54984 24 0 0 25 0 1 0 479990553 36687872 8444 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8957 8444 603 41 0 8916 0
vsize: 35828
[startup+560.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 8994 0 0 0 55983 25 0 0 25 0 1 0 479990553 38805504 8955 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9474 8955 603 41 0 9433 0
vsize: 37896
[startup+570.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 9060 0 0 0 56983 25 0 0 25 0 1 0 479990553 39084032 9020 4294967295 134512640 134672761 3221224528 3221223712 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9542 9020 603 41 0 9501 0
vsize: 38168
[startup+580.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 9111 0 0 0 57984 25 0 0 25 0 1 0 479990553 39346176 9071 4294967295 134512640 134672761 3221224528 3221223712 134615671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9606 9071 603 41 0 9565 0
vsize: 38424
[startup+590.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 9638 0 0 0 58982 28 0 0 25 0 1 0 479990553 41447424 9598 4294967295 134512640 134672761 3221224528 3221223712 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10119 9598 603 41 0 10078 0
vsize: 40476
[startup+600.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 10114 0 0 0 59981 28 0 0 25 0 1 0 479990553 43413504 10074 4294967295 134512640 134672761 3221224528 3221223712 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10599 10074 603 41 0 10558 0
vsize: 42396
[startup+610.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 10337 0 0 0 60981 29 0 0 25 0 1 0 479990553 44331008 10297 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10823 10297 603 41 0 10782 0
vsize: 43292
[startup+620.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 10698 0 0 0 61979 30 0 0 25 0 1 0 479990553 45776896 10658 4294967295 134512640 134672761 3221224528 3221223712 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11176 10658 603 41 0 11135 0
vsize: 44704
[startup+630.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 11003 0 0 0 62978 32 0 0 25 0 1 0 479990553 47087616 10963 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11496 10963 603 41 0 11455 0
vsize: 45984
[startup+640.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 11314 0 0 0 63977 33 0 0 25 0 1 0 479990553 48414720 11274 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11820 11274 603 41 0 11779 0
vsize: 47280
[startup+650.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 11609 0 0 0 64977 33 0 0 25 0 1 0 479990553 49582080 11569 4294967295 134512640 134672761 3221224528 3221223712 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12105 11569 603 41 0 12064 0
vsize: 48420
[startup+660.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 11609 0 0 0 65977 33 0 0 25 0 1 0 479990553 49582080 11569 4294967295 134512640 134672761 3221224528 3221223712 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12105 11569 603 41 0 12064 0
vsize: 48420
[startup+670.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 11609 0 0 0 66977 33 0 0 25 0 1 0 479990553 49582080 11569 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12105 11569 603 41 0 12064 0
vsize: 48420
[startup+680.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 11609 0 0 0 67977 33 0 0 25 0 1 0 479990553 49582080 11569 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12105 11569 603 41 0 12064 0
vsize: 48420
[startup+690.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 11609 0 0 0 68978 33 0 0 25 0 1 0 479990553 49582080 11569 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12105 11569 603 41 0 12064 0
vsize: 48420
[startup+700.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 11609 0 0 0 69978 33 0 0 25 0 1 0 479990553 49582080 11569 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12105 11569 603 41 0 12064 0
vsize: 48420
[startup+710.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 11620 0 0 0 70978 33 0 0 25 0 1 0 479990553 49618944 11579 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12114 11579 603 41 0 12073 0
vsize: 48456
[startup+720.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 11620 0 0 0 71978 33 0 0 25 0 1 0 479990553 49618944 11579 4294967295 134512640 134672761 3221224528 3221223712 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12114 11579 603 41 0 12073 0
vsize: 48456
[startup+730.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 11620 0 0 0 72978 33 0 0 25 0 1 0 479990553 49618944 11579 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12114 11579 603 41 0 12073 0
vsize: 48456
[startup+740.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 11621 0 0 0 73979 33 0 0 25 0 1 0 479990553 49618944 11580 4294967295 134512640 134672761 3221224528 3221223712 134615564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12114 11580 603 41 0 12073 0
vsize: 48456
[startup+750.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 11621 0 0 0 74979 33 0 0 25 0 1 0 479990553 49618944 11580 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12114 11580 603 41 0 12073 0
vsize: 48456
[startup+760.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 11622 0 0 0 75979 33 0 0 25 0 1 0 479990553 49618944 11581 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12114 11581 603 41 0 12073 0
vsize: 48456
[startup+770.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 11622 0 0 0 76979 33 0 0 25 0 1 0 479990553 49618944 11581 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12114 11581 603 41 0 12073 0
vsize: 48456
[startup+780.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 11622 0 0 0 77979 33 0 0 25 0 1 0 479990553 49618944 11581 4294967295 134512640 134672761 3221224528 3221223712 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12114 11581 603 41 0 12073 0
vsize: 48456
[startup+790.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 11622 0 0 0 78979 33 0 0 25 0 1 0 479990553 49618944 11581 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12114 11581 603 41 0 12073 0
vsize: 48456
[startup+800.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 11622 0 0 0 79980 33 0 0 25 0 1 0 479990553 49618944 11581 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12114 11581 603 41 0 12073 0
vsize: 48456
[startup+810.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 11622 0 0 0 80980 33 0 0 25 0 1 0 479990553 49618944 11581 4294967295 134512640 134672761 3221224528 3221223712 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12114 11581 603 41 0 12073 0
vsize: 48456
[startup+820.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 11732 0 0 0 81980 34 0 0 25 0 1 0 479990553 50143232 11691 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12242 11691 603 41 0 12201 0
vsize: 48968
[startup+830.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 12099 0 0 0 82979 34 0 0 25 0 1 0 479990553 51585024 12058 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12594 12058 603 41 0 12553 0
vsize: 50376
[startup+840.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 12447 0 0 0 83979 35 0 0 25 0 1 0 479990553 52998144 12406 4294967295 134512640 134672761 3221224528 3221223712 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12939 12406 603 41 0 12898 0
vsize: 51756
[startup+850.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 12447 0 0 0 84979 35 0 0 25 0 1 0 479990553 52998144 12406 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12939 12406 603 41 0 12898 0
vsize: 51756
[startup+860.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 12447 0 0 0 85979 35 0 0 25 0 1 0 479990553 52998144 12406 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12939 12406 603 41 0 12898 0
vsize: 51756
[startup+870.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 12447 0 0 0 86979 35 0 0 25 0 1 0 479990553 52998144 12406 4294967295 134512640 134672761 3221224528 3221223712 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12939 12406 603 41 0 12898 0
vsize: 51756
[startup+880.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 12448 0 0 0 87980 35 0 0 25 0 1 0 479990553 52998144 12407 4294967295 134512640 134672761 3221224528 3221223712 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12939 12407 603 41 0 12898 0
vsize: 51756
[startup+890.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 12463 0 0 0 88980 35 0 0 25 0 1 0 479990553 53063680 12421 4294967295 134512640 134672761 3221224528 3221223520 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12421 603 41 0 12914 0
vsize: 51820
[startup+900.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 12463 0 0 0 89980 35 0 0 25 0 1 0 479990553 53063680 12421 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12421 603 41 0 12914 0
vsize: 51820
[startup+910.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 12463 0 0 0 90980 35 0 0 25 0 1 0 479990553 53063680 12421 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12421 603 41 0 12914 0
vsize: 51820
[startup+920.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 12463 0 0 0 91980 35 0 0 25 0 1 0 479990553 53063680 12421 4294967295 134512640 134672761 3221224528 3221223568 134614348 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12421 603 41 0 12914 0
vsize: 51820
[startup+930.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 12463 0 0 0 92980 35 0 0 25 0 1 0 479990553 53063680 12421 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12421 603 41 0 12914 0
vsize: 51820
[startup+940.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 12463 0 0 0 93981 35 0 0 25 0 1 0 479990553 53063680 12421 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12421 603 41 0 12914 0
vsize: 51820
[startup+950.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 12463 0 0 0 94981 35 0 0 25 0 1 0 479990553 53063680 12421 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12421 603 41 0 12914 0
vsize: 51820
[startup+960.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 12464 0 0 0 95981 35 0 0 25 0 1 0 479990553 53063680 12422 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12422 603 41 0 12914 0
vsize: 51820
[startup+970.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 12464 0 0 0 96981 35 0 0 25 0 1 0 479990553 53063680 12422 4294967295 134512640 134672761 3221224528 3221223712 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12422 603 41 0 12914 0
vsize: 51820
[startup+980.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 12464 0 0 0 97981 35 0 0 25 0 1 0 479990553 53063680 12422 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12422 603 41 0 12914 0
vsize: 51820
[startup+990.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 12464 0 0 0 98982 35 0 0 25 0 1 0 479990553 53063680 12422 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12422 603 41 0 12914 0
vsize: 51820
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 12464 0 0 0 99983 35 0 0 25 0 1 0 479990553 53063680 12422 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12422 603 41 0 12914 0
vsize: 51820
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 12464 0 0 0 100983 35 0 0 25 0 1 0 479990553 53063680 12422 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12422 603 41 0 12914 0
vsize: 51820
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 12464 0 0 0 101983 35 0 0 25 0 1 0 479990553 53063680 12422 4294967295 134512640 134672761 3221224528 3221223712 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12422 603 41 0 12914 0
vsize: 51820
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 12464 0 0 0 102984 35 0 0 25 0 1 0 479990553 53063680 12422 4294967295 134512640 134672761 3221224528 3221223712 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12422 603 41 0 12914 0
vsize: 51820
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 12464 0 0 0 103984 35 0 0 25 0 1 0 479990553 53063680 12422 4294967295 134512640 134672761 3221224528 3221223712 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12422 603 41 0 12914 0
vsize: 51820
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 12464 0 0 0 104984 35 0 0 25 0 1 0 479990553 53063680 12422 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12422 603 41 0 12914 0
vsize: 51820
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 12464 0 0 0 105984 35 0 0 25 0 1 0 479990553 53063680 12422 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12422 603 41 0 12914 0
vsize: 51820
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 12464 0 0 0 106984 35 0 0 25 0 1 0 479990553 53063680 12422 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12422 603 41 0 12914 0
vsize: 51820
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 12464 0 0 0 107985 35 0 0 25 0 1 0 479990553 53063680 12422 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12422 603 41 0 12914 0
vsize: 51820
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 12464 0 0 0 108985 35 0 0 25 0 1 0 479990553 53063680 12422 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12422 603 41 0 12914 0
vsize: 51820
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 12464 0 0 0 109985 35 0 0 25 0 1 0 479990553 53063680 12422 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12422 603 41 0 12914 0
vsize: 51820
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 12464 0 0 0 110986 35 0 0 25 0 1 0 479990553 53063680 12422 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12422 603 41 0 12914 0
vsize: 51820
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 12464 0 0 0 111986 35 0 0 25 0 1 0 479990553 53063680 12422 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12422 603 41 0 12914 0
vsize: 51820
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 12464 0 0 0 112986 35 0 0 25 0 1 0 479990553 53063680 12422 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12422 603 41 0 12914 0
vsize: 51820
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 12464 0 0 0 113986 35 0 0 25 0 1 0 479990553 53063680 12422 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12422 603 41 0 12914 0
vsize: 51820
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 12464 0 0 0 114987 35 0 0 25 0 1 0 479990553 53063680 12422 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12422 603 41 0 12914 0
vsize: 51820
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27454
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 12464 0 0 0 115987 35 0 0 25 0 1 0 479990553 53063680 12422 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12422 603 41 0 12914 0
vsize: 51820
[startup+1170.03 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 27507
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 12464 0 0 0 116987 35 0 0 25 0 1 0 479990553 53063680 12422 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12422 603 41 0 12914 0
vsize: 51820
[startup+1180.03 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 27507
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 12464 0 0 0 117987 35 0 0 25 0 1 0 479990553 53063680 12422 4294967295 134512640 134672761 3221224528 3221223712 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12422 603 41 0 12914 0
vsize: 51820
[startup+1190.03 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 27507
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 12464 0 0 0 118987 35 0 0 25 0 1 0 479990553 53063680 12422 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12422 603 41 0 12914 0
vsize: 51820
[startup+1200.04 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 27507
Raw data (stat): 27454 (minisat+) R 27453 22612 22611 0 -1 0 12464 0 0 0 119987 35 0 0 25 0 1 0 479990553 53063680 12422 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12955 12422 603 41 0 12914 0
vsize: 51820
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.04 0.99 0.91 1/54 27507
Raw data (stat): 27454 (minisat+) Z 27453 22612 22611 0 -1 12 12464 0 0 0 119987 37 0 0 25 0 1 0 479990553 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.88
CPU system time (s): 0.378942
CPU usage (%): 100.016
Max. virtual memory (Kb): 51820
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####