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-chnl35_40_pb.cnf.cr.opb
MD5SUM	85d4e2fa5fd7a61a85d3ecb1e311bddb
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	0
Biggest coefficient in the objective function	0
Number of bits for the biggest coefficient in the objective function	0
Sum of the numbers in the objective function	0
Number of bits of the sum of numbers in the objective function	0
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	41
Number of bits of the biggest sum of numbers	6
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.083986
Number of variables	2800
Total number of constraints	150
Number of constraints which are clauses	80
Number of constraints which are cardinality constraints (but not clauses)	70
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	35
Maximum length of a constraint	40
Trace number 5335

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc20 THE 2005-04-13 23:34:17 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3775 boxname=wulflinc20 idbench=15 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  85d4e2fa5fd7a61a85d3ecb1e311bddb  /oldhome/oroussel/tmp/wulflinc20/normalized-chnl35_40_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc20/normalized-chnl35_40_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc20/normalized-chnl35_40_pb.cnf.cr.opb
IDLAUNCH: 3775
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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.215
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:        890720 kB
Buffers:         33816 kB
Cached:          74728 kB
SwapCached:       2636 kB
Active:          47912 kB
Inactive:        66124 kB
HighTotal:      131008 kB
HighFree:        52556 kB
LowTotal:       903652 kB
LowFree:        838164 kB
SwapTotal:     2097892 kB
SwapFree:      2095256 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            24268 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 23:54:19 (client local time) WITH STATUS 0 IN 1200.24 SECONDS
stats: 3775 7 1200.24 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 150 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ................................................................................
c ---[  69]---> BDD-cost:   77
c ---[  68]---> BDD-cost:   77
c ---[  67]---> BDD-cost:   77
c ---[  66]---> BDD-cost:   77
c ---[  65]---> BDD-cost:   77
c ---[  64]---> BDD-cost:   77
c ---[  63]---> BDD-cost:   77
c ---[  62]---> BDD-cost:   77
c ---[  61]---> BDD-cost:   77
c ---[  60]---> BDD-cost:   77
c ---[  59]---> BDD-cost:   77
c ---[  58]---> BDD-cost:   77
c ---[  57]---> BDD-cost:   77
c ---[  56]---> BDD-cost:   77
c ---[  55]---> BDD-cost:   77
c ---[  54]---> BDD-cost:   77
c ---[  53]---> BDD-cost:   77
c ---[  52]---> BDD-cost:   77
c ---[  51]---> BDD-cost:   77
c ---[  50]---> BDD-cost:   77
c ---[  49]---> BDD-cost:   77
c ---[  48]---> BDD-cost:   77
c ---[  47]---> BDD-cost:   77
c ---[  46]---> BDD-cost:   77
c ---[  45]---> BDD-cost:   77
c ---[  44]---> BDD-cost:   77
c ---[  43]---> BDD-cost:   77
c ---[  42]---> BDD-cost:   77
c ---[  41]---> BDD-cost:   77
c ---[  40]---> BDD-cost:   77
c ---[  39]---> BDD-cost:   77
c ---[  38]---> BDD-cost:   77
c ---[  37]---> BDD-cost:   77
c ---[  36]---> BDD-cost:   77
c ---[  35]---> BDD-cost:   77
c ---[  34]---> BDD-cost:   77
c ---[  33]---> BDD-cost:   77
c ---[  32]---> BDD-cost:   77
c ---[  31]---> BDD-cost:   77
c ---[  30]---> BDD-cost:   77
c ---[  29]---> BDD-cost:   77
c ---[  28]---> BDD-cost:   77
c ---[  27]---> BDD-cost:   77
c ---[  26]---> BDD-cost:   77
c ---[  25]---> BDD-cost:   77
c ---[  24]---> BDD-cost:   77
c ---[  23]---> BDD-cost:   77
c ---[  22]---> BDD-cost:   77
c ---[  21]---> BDD-cost:   77
c ---[  20]---> BDD-cost:   77
c ---[  19]---> BDD-cost:   77
c ---[  18]---> BDD-cost:   77
c ---[  17]---> BDD-cost:   77
c ---[  16]---> BDD-cost:   77
c ---[  15]---> BDD-cost:   77
c ---[  14]---> BDD-cost:   77
c ---[  13]---> BDD-cost:   77
c ---[  12]---> BDD-cost:   77
c ---[  11]---> BDD-cost:   77
c ---[  10]---> BDD-cost:   77
c ---[   9]---> BDD-cost:   77
c ---[   8]---> BDD-cost:   77
c ---[   7]---> BDD-cost:   77
c ---[   6]---> BDD-cost:   77
c ---[   5]---> BDD-cost:   77
c ---[   4]---> BDD-cost:   77
c ---[   3]---> BDD-cost:   77
c ---[   2]---> BDD-cost:   77
c ---[   1]---> BDD-cost:   77
c ---[   0]---> BDD-cost:   77
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   13450    37590 |    4034       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/8120          
c   -- var.elim.:  2000/8120          
c   -- var.elim.:  3000/8120          
c   -- var.elim.:  4000/8120          
c   -- var.elim.:  5000/8120          
c   -- var.elim.:  6000/8120          
c   -- var.elim.:  7000/8120          
c   -- var.elim.:  8000/8120          
c   -- var.elim.:  8120/8120          
c   -- var.elim.:  1000/3096          
c   -- var.elim.:  2000/3096          
c   -- var.elim.:  3000/3096          
c   -- var.elim.:  3096/3096          
c   -- var.elim.:  146/146          
c   -- subsuming                       
c   -- var.elim.:  1000/1806          
c   -- var.elim.:  1806/1806          
c   -- var.elim.:  680/680          
c   -- var.elim.:  224/224          
c   -- var.elim.:  222/222          
c   -- var.elim.:  98/98          
c   -- var.elim.:  90/90          
c   -- var.elim.:  92/92          
c   -- var.elim.:  94/94          
c   -- var.elim.:  96/96          
c   -- var.elim.:  98/98          
c   -- var.elim.:  100/100          
c   -- var.elim.:  102/102          
c   -- var.elim.:  104/104          
c   -- var.elim.:  106/106          
c   -- var.elim.:  108/108          
c   -- var.elim.:  110/110          
c   -#### 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 31803
Raw data (stat): 31803 (runsolver) R 31802 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479946473 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 3579 0 0 0 989 9 0 0 25 0 1 0 479946473 16732160 3522 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4085 3522 603 41 0 4044 0
vsize: 16340
[startup+20.0001 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 5197 0 0 0 1985 13 0 0 25 0 1 0 479946473 23228416 5140 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5671 5140 603 41 0 5630 0
vsize: 22684
[startup+30.0008 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 5725 0 0 0 2984 14 0 0 25 0 1 0 479946473 25456640 5668 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6215 5668 603 41 0 6174 0
vsize: 24860
[startup+40.0003 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 6061 0 0 0 3984 15 0 0 25 0 1 0 479946473 26890240 6004 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6565 6004 603 41 0 6524 0
vsize: 26260
[startup+50.0003 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 7124 0 0 0 4982 17 0 0 25 0 1 0 479946473 31264768 7067 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7633 7067 603 41 0 7592 0
vsize: 30532
[startup+60.001 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 7175 0 0 0 5982 17 0 0 25 0 1 0 479946473 31432704 7117 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7674 7117 603 41 0 7633 0
vsize: 30696
[startup+70.0004 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 8390 0 0 0 6979 20 0 0 25 0 1 0 479946473 36417536 8332 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8891 8332 603 41 0 8850 0
vsize: 35564
[startup+80.0014 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 8390 0 0 0 7979 20 0 0 25 0 1 0 479946473 36417536 8332 4294967295 134512640 134672761 3221224544 3221223584 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8891 8332 603 41 0 8850 0
vsize: 35564
[startup+90.0012 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 9304 0 0 0 8975 24 0 0 25 0 1 0 479946473 40235008 9246 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9823 9246 603 41 0 9782 0
vsize: 39292
[startup+100.001 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 9681 0 0 0 9974 25 0 0 25 0 1 0 479946473 41705472 9622 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10182 9622 603 41 0 10141 0
vsize: 40728
[startup+110.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 9683 0 0 0 10974 26 0 0 25 0 1 0 479946473 41705472 9624 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10182 9624 603 41 0 10141 0
vsize: 40728
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 9683 0 0 0 11974 26 0 0 25 0 1 0 479946473 41705472 9624 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10182 9624 603 41 0 10141 0
vsize: 40728
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 9684 0 0 0 12975 26 0 0 25 0 1 0 479946473 41705472 9625 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10182 9625 603 41 0 10141 0
vsize: 40728
[startup+140.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 9684 0 0 0 13975 26 0 0 25 0 1 0 479946473 41705472 9625 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10182 9625 603 41 0 10141 0
vsize: 40728
[startup+150.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 9693 0 0 0 14975 26 0 0 25 0 1 0 479946473 41734144 9633 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10189 9633 603 41 0 10148 0
vsize: 40756
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 9693 0 0 0 15975 26 0 0 25 0 1 0 479946473 41734144 9633 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10189 9633 603 41 0 10148 0
vsize: 40756
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 9693 0 0 0 16975 26 0 0 25 0 1 0 479946473 41734144 9633 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10189 9633 603 41 0 10148 0
vsize: 40756
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 9701 0 0 0 17975 26 0 0 25 0 1 0 479946473 41734144 9641 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10189 9641 603 41 0 10148 0
vsize: 40756
[startup+190.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 10098 0 0 0 18974 28 0 0 25 0 1 0 479946473 43352064 10037 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10584 10037 603 41 0 10543 0
vsize: 42336
[startup+200.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 10098 0 0 0 19974 28 0 0 25 0 1 0 479946473 43352064 10037 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10584 10037 603 41 0 10543 0
vsize: 42336
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 10098 0 0 0 20974 28 0 0 25 0 1 0 479946473 43343872 10036 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10582 10036 603 41 0 10541 0
vsize: 42328
[startup+220.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 10098 0 0 0 21974 28 0 0 25 0 1 0 479946473 43343872 10036 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10582 10036 603 41 0 10541 0
vsize: 42328
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 10098 0 0 0 22974 28 0 0 25 0 1 0 479946473 43343872 10036 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10582 10036 603 41 0 10541 0
vsize: 42328
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 10098 0 0 0 23974 28 0 0 25 0 1 0 479946473 43343872 10036 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10582 10036 603 41 0 10541 0
vsize: 42328
[startup+250.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 10098 0 0 0 24974 28 0 0 25 0 1 0 479946473 43343872 10036 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10582 10036 603 41 0 10541 0
vsize: 42328
[startup+260.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 11093 0 0 0 25972 31 0 0 25 0 1 0 479946473 47525888 11031 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11603 11031 603 41 0 11562 0
vsize: 46412
[startup+270.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 11625 0 0 0 26970 32 0 0 25 0 1 0 479946473 49643520 11563 4294967295 134512640 134672761 3221224544 3221223744 134610644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12120 11563 603 41 0 12079 0
vsize: 48480
[startup+280.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 11625 0 0 0 27971 32 0 0 25 0 1 0 479946473 49643520 11563 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12120 11563 603 41 0 12079 0
vsize: 48480
[startup+290.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 11625 0 0 0 28971 33 0 0 25 0 1 0 479946473 49643520 11563 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12120 11563 603 41 0 12079 0
vsize: 48480
[startup+300.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 11625 0 0 0 29971 33 0 0 25 0 1 0 479946473 49643520 11563 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12120 11563 603 41 0 12079 0
vsize: 48480
[startup+310.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 11625 0 0 0 30971 33 0 0 25 0 1 0 479946473 49643520 11563 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12120 11563 603 41 0 12079 0
vsize: 48480
[startup+320.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 11625 0 0 0 31971 33 0 0 25 0 1 0 479946473 49639424 11562 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12119 11562 603 41 0 12078 0
vsize: 48476
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 11625 0 0 0 32971 33 0 0 25 0 1 0 479946473 49639424 11562 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12119 11562 603 41 0 12078 0
vsize: 48476
[startup+340.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 11625 0 0 0 33971 33 0 0 25 0 1 0 479946473 49639424 11562 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12119 11562 603 41 0 12078 0
vsize: 48476
[startup+350.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 11625 0 0 0 34971 33 0 0 25 0 1 0 479946473 49639424 11562 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12119 11562 603 41 0 12078 0
vsize: 48476
[startup+360.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 11625 0 0 0 35972 33 0 0 25 0 1 0 479946473 49639424 11562 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12119 11562 603 41 0 12078 0
vsize: 48476
[startup+370.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 11625 0 0 0 36972 33 0 0 25 0 1 0 479946473 49639424 11562 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12119 11562 603 41 0 12078 0
vsize: 48476
[startup+380.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 11625 0 0 0 37972 33 0 0 25 0 1 0 479946473 49639424 11562 4294967295 134512640 134672761 3221224544 3221223680 134614583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12119 11562 603 41 0 12078 0
vsize: 48476
[startup+390.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 11625 0 0 0 38972 33 0 0 25 0 1 0 479946473 49639424 11562 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12119 11562 603 41 0 12078 0
vsize: 48476
[startup+400.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 11830 0 0 0 39971 34 0 0 25 0 1 0 479946473 50565120 11767 4294967295 134512640 134672761 3221224544 3221223584 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12345 11767 603 41 0 12304 0
vsize: 49380
[startup+410.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 12192 0 0 0 40970 36 0 0 25 0 1 0 479946473 51978240 12128 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12690 12128 603 41 0 12649 0
vsize: 50760
[startup+420.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 12192 0 0 0 41970 36 0 0 25 0 1 0 479946473 51978240 12128 4294967295 134512640 134672761 3221224544 3221223536 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12690 12128 603 41 0 12649 0
vsize: 50760
[startup+430.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 12192 0 0 0 42970 36 0 0 25 0 1 0 479946473 51978240 12128 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12690 12128 603 41 0 12649 0
vsize: 50760
[startup+440.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 12192 0 0 0 43970 36 0 0 25 0 1 0 479946473 51978240 12128 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12690 12128 603 41 0 12649 0
vsize: 50760
[startup+450.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 12192 0 0 0 44970 36 0 0 25 0 1 0 479946473 51978240 12128 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12690 12128 603 41 0 12649 0
vsize: 50760
[startup+460.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 12207 0 0 0 45970 36 0 0 25 0 1 0 479946473 52174848 12143 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12738 12143 603 41 0 12697 0
vsize: 50952
[startup+470.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 12584 0 0 0 46969 38 0 0 25 0 1 0 479946473 53616640 12520 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13090 12520 603 41 0 13049 0
vsize: 52360
[startup+480.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 12584 0 0 0 47969 38 0 0 25 0 1 0 479946473 53616640 12520 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13090 12520 603 41 0 13049 0
vsize: 52360
[startup+490.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 12584 0 0 0 48969 38 0 0 25 0 1 0 479946473 53616640 12520 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13090 12520 603 41 0 13049 0
vsize: 52360
[startup+500.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 12584 0 0 0 49969 38 0 0 25 0 1 0 479946473 53616640 12520 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13090 12520 603 41 0 13049 0
vsize: 52360
[startup+510.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 12933 0 0 0 50969 39 0 0 25 0 1 0 479946473 55062528 12869 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13443 12869 603 41 0 13402 0
vsize: 53772
[startup+520.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 13797 0 0 0 51967 41 0 0 25 0 1 0 479946473 58580992 13733 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14302 13733 603 41 0 14261 0
vsize: 57208
[startup+530.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 13797 0 0 0 52967 41 0 0 25 0 1 0 479946473 58580992 13733 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14302 13733 603 41 0 14261 0
vsize: 57208
[startup+540.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 13797 0 0 0 53967 41 0 0 25 0 1 0 479946473 58580992 13733 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14302 13733 603 41 0 14261 0
vsize: 57208
[startup+550.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 13797 0 0 0 54967 41 0 0 25 0 1 0 479946473 58580992 13733 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14302 13733 603 41 0 14261 0
vsize: 57208
[startup+560.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 13797 0 0 0 55967 41 0 0 25 0 1 0 479946473 58580992 13733 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14302 13733 603 41 0 14261 0
vsize: 57208
[startup+570.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 14123 0 0 0 56967 42 0 0 25 0 1 0 479946473 59957248 14059 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14638 14059 603 41 0 14597 0
vsize: 58552
[startup+580.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 14574 0 0 0 57966 42 0 0 25 0 1 0 479946473 61890560 14510 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15110 14510 603 41 0 15069 0
vsize: 60440
[startup+590.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 15120 0 0 0 58965 44 0 0 25 0 1 0 479946473 64204800 15056 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15675 15056 603 41 0 15634 0
vsize: 62700
[startup+600.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 15651 0 0 0 59964 45 0 0 25 0 1 0 479946473 66420736 15587 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16216 15587 603 41 0 16175 0
vsize: 64864
[startup+610.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 16005 0 0 0 60963 46 0 0 25 0 1 0 479946473 67903488 15941 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16578 15941 603 41 0 16537 0
vsize: 66312
[startup+620.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 16471 0 0 0 61962 48 0 0 25 0 1 0 479946473 69869568 16407 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17058 16407 603 41 0 17017 0
vsize: 68232
[startup+630.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 16984 0 0 0 62960 49 0 0 25 0 1 0 479946473 71979008 16920 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17573 16920 603 41 0 17532 0
vsize: 70292
[startup+640.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 17145 0 0 0 63960 50 0 0 25 0 1 0 479946473 72560640 17080 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17715 17080 603 41 0 17674 0
vsize: 70860
[startup+650.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 17147 0 0 0 64960 50 0 0 25 0 1 0 479946473 72560640 17082 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17715 17082 603 41 0 17674 0
vsize: 70860
[startup+660.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 17152 0 0 0 65960 50 0 0 25 0 1 0 479946473 72560640 17087 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17715 17087 603 41 0 17674 0
vsize: 70860
[startup+670.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 17153 0 0 0 66960 50 0 0 25 0 1 0 479946473 72560640 17088 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17715 17088 603 41 0 17674 0
vsize: 70860
[startup+680.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 17153 0 0 0 67961 50 0 0 25 0 1 0 479946473 72560640 17088 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17715 17088 603 41 0 17674 0
vsize: 70860
[startup+690.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 17155 0 0 0 68961 50 0 0 25 0 1 0 479946473 72560640 17090 4294967295 134512640 134672761 3221224544 3221223416 1075353028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17715 17090 603 41 0 17674 0
vsize: 70860
[startup+700.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 17158 0 0 0 69961 50 0 0 25 0 1 0 479946473 72560640 17093 4294967295 134512640 134672761 3221224544 3221223680 134614513 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17715 17093 603 41 0 17674 0
vsize: 70860
[startup+710.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 17158 0 0 0 70961 50 0 0 25 0 1 0 479946473 72560640 17093 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17715 17093 603 41 0 17674 0
vsize: 70860
[startup+720.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 17158 0 0 0 71961 50 0 0 25 0 1 0 479946473 72560640 17093 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17715 17093 603 41 0 17674 0
vsize: 70860
[startup+730.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 17158 0 0 0 72961 50 0 0 25 0 1 0 479946473 72560640 17093 4294967295 134512640 134672761 3221224544 3221223312 1075352301 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17715 17093 603 41 0 17674 0
vsize: 70860
[startup+740.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 17161 0 0 0 73962 50 0 0 25 0 1 0 479946473 72560640 17096 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17715 17096 603 41 0 17674 0
vsize: 70860
[startup+750.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 17164 0 0 0 74962 50 0 0 25 0 1 0 479946473 72560640 17099 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17715 17099 603 41 0 17674 0
vsize: 70860
[startup+760.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 17164 0 0 0 75962 50 0 0 25 0 1 0 479946473 72560640 17099 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17715 17099 603 41 0 17674 0
vsize: 70860
[startup+770.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 17168 0 0 0 76962 50 0 0 25 0 1 0 479946473 72560640 17103 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17715 17103 603 41 0 17674 0
vsize: 70860
[startup+780.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 17448 0 0 0 77962 51 0 0 25 0 1 0 479946473 73768960 17383 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18010 17383 603 41 0 17969 0
vsize: 72040
[startup+790.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 17858 0 0 0 78960 53 0 0 25 0 1 0 479946473 75481088 17793 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18428 17793 603 41 0 18387 0
vsize: 73712
[startup+800.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 18046 0 0 0 79960 53 0 0 25 0 1 0 479946473 76267520 17981 4294967295 134512640 134672761 3221224544 3221223728 134615926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18620 17981 603 41 0 18579 0
vsize: 74480
[startup+810.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 18241 0 0 0 80960 54 0 0 25 0 1 0 479946473 77131776 18176 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18831 18176 603 41 0 18790 0
vsize: 75324
[startup+820.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 18347 0 0 0 81960 54 0 0 25 0 1 0 479946473 77512704 18282 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18924 18282 603 41 0 18883 0
vsize: 75696
[startup+830.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 18347 0 0 0 82960 54 0 0 25 0 1 0 479946473 77512704 18282 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18924 18282 603 41 0 18883 0
vsize: 75696
[startup+840.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 18347 0 0 0 83960 54 0 0 25 0 1 0 479946473 77512704 18282 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18924 18282 603 41 0 18883 0
vsize: 75696
[startup+850.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 18347 0 0 0 84960 54 0 0 25 0 1 0 479946473 77512704 18282 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18924 18282 603 41 0 18883 0
vsize: 75696
[startup+860.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 18347 0 0 0 85960 54 0 0 25 0 1 0 479946473 77512704 18282 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18924 18282 603 41 0 18883 0
vsize: 75696
[startup+870.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 18347 0 0 0 86960 54 0 0 25 0 1 0 479946473 77512704 18282 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18924 18282 603 41 0 18883 0
vsize: 75696
[startup+880.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 18347 0 0 0 87960 54 0 0 25 0 1 0 479946473 77512704 18282 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18924 18282 603 41 0 18883 0
vsize: 75696
[startup+890.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 18347 0 0 0 88960 55 0 0 25 0 1 0 479946473 77512704 18282 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18924 18282 603 41 0 18883 0
vsize: 75696
[startup+900.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 18347 0 0 0 89960 55 0 0 25 0 1 0 479946473 77512704 18282 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18924 18282 603 41 0 18883 0
vsize: 75696
[startup+910.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 18347 0 0 0 90960 55 0 0 25 0 1 0 479946473 77512704 18282 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18924 18282 603 41 0 18883 0
vsize: 75696
[startup+920.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 18351 0 0 0 91960 55 0 0 25 0 1 0 479946473 77512704 18286 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18924 18286 603 41 0 18883 0
vsize: 75696
[startup+930.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 18353 0 0 0 92960 55 0 0 25 0 1 0 479946473 77512704 18288 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18924 18288 603 41 0 18883 0
vsize: 75696
[startup+940.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 18353 0 0 0 93961 55 0 0 25 0 1 0 479946473 77512704 18288 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18924 18288 603 41 0 18883 0
vsize: 75696
[startup+950.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 18381 0 0 0 94961 55 0 0 25 0 1 0 479946473 77627392 18316 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18952 18316 603 41 0 18911 0
vsize: 75808
[startup+960.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 18381 0 0 0 95961 55 0 0 25 0 1 0 479946473 77627392 18316 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18952 18316 603 41 0 18911 0
vsize: 75808
[startup+970.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 18381 0 0 0 96961 55 0 0 25 0 1 0 479946473 77627392 18316 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18952 18316 603 41 0 18911 0
vsize: 75808
[startup+980.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 18381 0 0 0 97961 55 0 0 25 0 1 0 479946473 77627392 18316 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18952 18316 603 41 0 18911 0
vsize: 75808
[startup+990.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 18382 0 0 0 98961 55 0 0 25 0 1 0 479946473 77627392 18317 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18952 18317 603 41 0 18911 0
vsize: 75808
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 18382 0 0 0 99961 55 0 0 25 0 1 0 479946473 77627392 18317 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18952 18317 603 41 0 18911 0
vsize: 75808
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 18382 0 0 0 100961 55 0 0 25 0 1 0 479946473 77627392 18317 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18952 18317 603 41 0 18911 0
vsize: 75808
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 18384 0 0 0 101961 55 0 0 25 0 1 0 479946473 77627392 18319 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18952 18319 603 41 0 18911 0
vsize: 75808
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 18384 0 0 0 102961 55 0 0 25 0 1 0 479946473 77627392 18319 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18952 18319 603 41 0 18911 0
vsize: 75808
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 18384 0 0 0 103962 55 0 0 25 0 1 0 479946473 77627392 18319 4294967295 134512640 134672761 3221224544 3221223636 1075351193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18952 18319 603 41 0 18911 0
vsize: 75808
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 18385 0 0 0 104962 56 0 0 25 0 1 0 479946473 77619200 18319 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18950 18319 603 41 0 18909 0
vsize: 75800
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 18385 0 0 0 105962 56 0 0 25 0 1 0 479946473 77619200 18319 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18950 18319 603 41 0 18909 0
vsize: 75800
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 18385 0 0 0 106962 56 0 0 25 0 1 0 479946473 77619200 18319 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18950 18319 603 41 0 18909 0
vsize: 75800
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 18385 0 0 0 107962 56 0 0 25 0 1 0 479946473 77619200 18319 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18950 18319 603 41 0 18909 0
vsize: 75800
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 18385 0 0 0 108962 56 0 0 25 0 1 0 479946473 77619200 18319 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18950 18319 603 41 0 18909 0
vsize: 75800
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 18385 0 0 0 109962 56 0 0 25 0 1 0 479946473 77619200 18319 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18950 18319 603 41 0 18909 0
vsize: 75800
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 18385 0 0 0 110962 56 0 0 25 0 1 0 479946473 77619200 18319 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18950 18319 603 41 0 18909 0
vsize: 75800
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 18385 0 0 0 111962 56 0 0 25 0 1 0 479946473 77619200 18319 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18950 18319 603 41 0 18909 0
vsize: 75800
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 18385 0 0 0 112962 56 0 0 25 0 1 0 479946473 77619200 18319 4294967295 134512640 134672761 3221224544 3221223584 134614191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18950 18319 603 41 0 18909 0
vsize: 75800
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 18385 0 0 0 113963 56 0 0 25 0 1 0 479946473 77619200 18319 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18950 18319 603 41 0 18909 0
vsize: 75800
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 18385 0 0 0 114963 56 0 0 25 0 1 0 479946473 77619200 18319 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18950 18319 603 41 0 18909 0
vsize: 75800
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 18385 0 0 0 115963 56 0 0 25 0 1 0 479946473 77619200 18319 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18950 18319 603 41 0 18909 0
vsize: 75800
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 18385 0 0 0 116963 57 0 0 25 0 1 0 479946473 77619200 18319 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18950 18319 603 41 0 18909 0
vsize: 75800
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 18385 0 0 0 117963 57 0 0 25 0 1 0 479946473 77619200 18319 4294967295 134512640 134672761 3221224544 3221223584 134612653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18950 18319 603 41 0 18909 0
vsize: 75800
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 18385 0 0 0 118963 57 0 0 25 0 1 0 479946473 77619200 18319 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18950 18319 603 41 0 18909 0
vsize: 75800
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 27565 27564 0 -1 0 18385 0 0 0 119963 57 0 0 25 0 1 0 479946473 77619200 18319 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18950 18319 603 41 0 18909 0
vsize: 75800
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 31803
Raw data (stat): 31803 (minisat+) Z 31802 27565 27564 0 -1 12 18385 0 0 0 119963 60 0 0 25 0 1 0 479946473 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.05
CPU time (s): 1200.24
CPU user time (s): 1199.64
CPU system time (s): 0.606907
CPU usage (%): 100.016
Max. virtual memory (Kb): 75808
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####