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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
  3. 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.
  4. 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

Namenormalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl15_25_pb.cnf.cr.opb
MD5SUM808390b13d2d87ec4e78f628ed3af9ba
Bench Categoryno optimization function (SAT)
Has Objective FunctionNO
SatisfiableNO
(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 26
Number of bits of the biggest sum of numbers5
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark0.021995
Number of variables750
Total number of constraints80
Number of constraints which are clauses50
Number of constraints which are cardinality constraints (but not clauses)30
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint15
Maximum length of a constraint25

Trace number 6085 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-04-14 03:21:09 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4519 boxname=wulflinc31 idbench=7 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  808390b13d2d87ec4e78f628ed3af9ba  /oldhome/oroussel/tmp/wulflinc31/normalized-chnl15_25_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc31/normalized-chnl15_25_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc31/normalized-chnl15_25_pb.cnf.cr.opb
IDLAUNCH: 4519
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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.153
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:        888456 kB
Buffers:         36240 kB
Cached:          71216 kB
SwapCached:        392 kB
Active:          52588 kB
Inactive:        58004 kB
HighTotal:      131008 kB
HighFree:        56084 kB
LowTotal:       903652 kB
LowFree:        832372 kB
SwapTotal:     2097892 kB
SwapFree:      2097452 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6832 kB
Slab:            29932 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 03:41:11 (client local time) WITH STATUS 0 IN 1200.16 SECONDS
stats: 4519 7 1200.16 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 80 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..................................................
c ---[  29]---> BDD-cost:   47
c ---[  28]---> BDD-cost:   47
c ---[  27]---> BDD-cost:   47
c ---[  26]---> BDD-cost:   47
c ---[  25]---> BDD-cost:   47
c ---[  24]---> BDD-cost:   47
c ---[  23]---> BDD-cost:   47
c ---[  22]---> BDD-cost:   47
c ---[  21]---> BDD-cost:   47
c ---[  20]---> BDD-cost:   47
c ---[  19]---> BDD-cost:   47
c ---[  18]---> BDD-cost:   47
c ---[  17]---> BDD-cost:   47
c ---[  16]---> BDD-cost:   47
c ---[  15]---> BDD-cost:   47
c ---[  14]---> BDD-cost:   47
c ---[  13]---> BDD-cost:   47
c ---[  12]---> BDD-cost:   47
c ---[  11]---> BDD-cost:   47
c ---[  10]---> BDD-cost:   47
c ---[   9]---> BDD-cost:   47
c ---[   8]---> BDD-cost:   47
c ---[   7]---> BDD-cost:   47
c ---[   6]---> BDD-cost:   47
c ---[   5]---> BDD-cost:   47
c ---[   4]---> BDD-cost:   47
c ---[   3]---> BDD-cost:   47
c ---[   2]---> BDD-cost:   47
c ---[   1]---> BDD-cost:   47
c ---[   0]---> BDD-cost:   47
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    6260    17940 |    2086       0        0     nan |  0.000 % |
c |       104 |    6215    17805 |    2294      88     4201    47.7 |  1.806 % |
c |       254 |    6180    17700 |    2524     212    12596    59.4 |  2.130 % |
c |       479 |    6175    17685 |    2776     435    29861    68.6 |  2.176 % |
c |       817 |    6165    17655 |    3054     766    58331    76.2 |  2.269 % |
c |      1323 |    6155    17625 |    3359    1268   107878    85.1 |  2.361 % |
c |      2082 |    6150    17610 |    3695    2025   189890    93.8 |  2.407 % |
c |      3224 |    6140    17580 |    4065    3164   336451   106.3 |  2.500 % |
c |      4933 |    6140    17580 |    4471    2663   312180   117.2 |  2.500 % |
c |      7498 |    6040    17280 |    4918    2694   230939    85.7 |  3.426 % |
c |     11342 |    5950    17010 |    5410    3924   386959    98.6 |  4.259 % |
c |     17109 |    5880    16800 |    5951    3848   389803   101.3 |  4.907 % |
c |     25759 |    5820    16620 |    6546    6130   744819   121.5 |  5.463 % |
c |     38733 |    5730    16350 |    7201    5282   555688   105.2 |  6.296 % |
c |     58195 |    5406    15380 |    7921    5495   640654   116.6 |  9.306 % |
c |     87389 |    5276    14990 |    8713    5187   540087   104.1 | 10.509 % |
c |    131182 |    4976    14090 |    9585    6902   694098   100.6 | 13.287 % |
c |    196869 |    4491    12635 |   10543    6228   616280    99.0 | 17.778 % |
c |    295395 |    4102    11470 |   11597    8870   936536   105.6 | 21.389 % |
c |    443184 |    3629    10055 |   12757    7325   833472   113.8 | 25.787 % |
c |    664868 |    3259     8955 |   14033   10235  1070680   104.6 | 29.259 % |
#### 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.96 0.91 2/54 30815
Raw data (stat): 30815 (runsolver) R 30814 23176 23175 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481295848 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+10 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 1267 0 0 0 995 2 0 0 25 0 1 0 481295848 6737920 1245 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1645 1245 603 41 0 1604 0
vsize: 6580
[startup+20.0005 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 1505 0 0 0 1994 3 0 0 25 0 1 0 481295848 7815168 1483 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1908 1483 603 41 0 1867 0
vsize: 7632
[startup+30.0008 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 1683 0 0 0 2993 4 0 0 25 0 1 0 481295848 8491008 1661 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2073 1661 603 41 0 2032 0
vsize: 8292
[startup+40.0015 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 1703 0 0 0 3992 4 0 0 25 0 1 0 481295848 8626176 1681 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2106 1681 603 41 0 2065 0
vsize: 8424
[startup+50.0021 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 1759 0 0 0 4993 4 0 0 25 0 1 0 481295848 8896512 1737 4294967295 134512640 134672761 3221224544 3221223648 134560252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2172 1737 603 41 0 2131 0
vsize: 8688
[startup+60.0024 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 1846 0 0 0 5993 4 0 0 25 0 1 0 481295848 9170944 1824 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2239 1824 603 41 0 2198 0
vsize: 8956
[startup+70.0033 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 2025 0 0 0 6992 5 0 0 25 0 1 0 481295848 9981952 2003 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2437 2003 603 41 0 2396 0
vsize: 9748
[startup+80.0039 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 2037 0 0 0 7992 5 0 0 25 0 1 0 481295848 9981952 2015 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2437 2015 603 41 0 2396 0
vsize: 9748
[startup+90.0042 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 2118 0 0 0 8992 5 0 0 25 0 1 0 481295848 10399744 2096 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2539 2096 603 41 0 2498 0
vsize: 10156
[startup+100.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 2133 0 0 0 9992 5 0 0 25 0 1 0 481295848 10563584 2111 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2579 2111 603 41 0 2538 0
vsize: 10316
[startup+110.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 2166 0 0 0 10992 6 0 0 25 0 1 0 481295848 10706944 2144 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2614 2144 603 41 0 2573 0
vsize: 10456
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 2211 0 0 0 11992 6 0 0 25 0 1 0 481295848 10842112 2189 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2647 2189 603 41 0 2606 0
vsize: 10588
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 2228 0 0 0 12993 6 0 0 25 0 1 0 481295848 11005952 2206 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2687 2206 603 41 0 2646 0
vsize: 10748
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 2228 0 0 0 13993 6 0 0 25 0 1 0 481295848 11005952 2206 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2687 2206 603 41 0 2646 0
vsize: 10748
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 2241 0 0 0 14993 6 0 0 25 0 1 0 481295848 11005952 2219 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2687 2219 603 41 0 2646 0
vsize: 10748
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 2247 0 0 0 15993 6 0 0 25 0 1 0 481295848 11005952 2225 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2687 2225 603 41 0 2646 0
vsize: 10748
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 2264 0 0 0 16993 6 0 0 25 0 1 0 481295848 11169792 2242 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2727 2242 603 41 0 2686 0
vsize: 10908
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 2295 0 0 0 17992 6 0 0 25 0 1 0 481295848 11313152 2273 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2762 2273 603 41 0 2721 0
vsize: 11048
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 2363 0 0 0 18991 7 0 0 25 0 1 0 481295848 11587584 2341 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2829 2341 603 41 0 2788 0
vsize: 11316
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 2397 0 0 0 19991 7 0 0 25 0 1 0 481295848 11722752 2375 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2862 2375 603 41 0 2821 0
vsize: 11448
[startup+210.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 2426 0 0 0 20991 7 0 0 25 0 1 0 481295848 11857920 2404 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2895 2404 603 41 0 2854 0
vsize: 11580
[startup+220.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 2502 0 0 0 21990 8 0 0 25 0 1 0 481295848 12124160 2480 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2960 2480 603 41 0 2919 0
vsize: 11840
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 2513 0 0 0 22991 8 0 0 25 0 1 0 481295848 12124160 2491 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2960 2491 603 41 0 2919 0
vsize: 11840
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 2528 0 0 0 23991 8 0 0 25 0 1 0 481295848 12259328 2506 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2993 2506 603 41 0 2952 0
vsize: 11972
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 2560 0 0 0 24991 8 0 0 25 0 1 0 481295848 12423168 2538 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3033 2538 603 41 0 2992 0
vsize: 12132
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 2565 0 0 0 25991 8 0 0 25 0 1 0 481295848 12423168 2543 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3033 2543 603 41 0 2992 0
vsize: 12132
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 2581 0 0 0 26991 8 0 0 25 0 1 0 481295848 12587008 2559 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3073 2559 603 41 0 3032 0
vsize: 12292
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 2586 0 0 0 27991 8 0 0 25 0 1 0 481295848 12587008 2564 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3073 2564 603 41 0 3032 0
vsize: 12292
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 2586 0 0 0 28991 8 0 0 25 0 1 0 481295848 12587008 2564 4294967295 134512640 134672761 3221224544 3221223728 134558394 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3073 2564 603 41 0 3032 0
vsize: 12292
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 2588 0 0 0 29991 8 0 0 25 0 1 0 481295848 12587008 2566 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3073 2566 603 41 0 3032 0
vsize: 12292
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 2588 0 0 0 30991 8 0 0 25 0 1 0 481295848 12587008 2566 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3073 2566 603 41 0 3032 0
vsize: 12292
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 2647 0 0 0 31991 8 0 0 25 0 1 0 481295848 12857344 2625 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3139 2625 603 41 0 3098 0
vsize: 12556
[startup+330.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 2657 0 0 0 32991 8 0 0 25 0 1 0 481295848 12857344 2635 4294967295 134512640 134672761 3221224544 3221223680 134565039 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3139 2635 603 41 0 3098 0
vsize: 12556
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 2707 0 0 0 33991 9 0 0 25 0 1 0 481295848 13144064 2685 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3209 2685 603 41 0 3168 0
vsize: 12836
[startup+350.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 2720 0 0 0 34991 9 0 0 25 0 1 0 481295848 13144064 2698 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3209 2698 603 41 0 3168 0
vsize: 12836
[startup+360.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 2741 0 0 0 35991 9 0 0 25 0 1 0 481295848 13279232 2719 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3242 2719 603 41 0 3201 0
vsize: 12968
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 2809 0 0 0 36991 9 0 0 25 0 1 0 481295848 13549568 2787 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3308 2787 603 41 0 3267 0
vsize: 13232
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 2835 0 0 0 37991 9 0 0 25 0 1 0 481295848 13697024 2813 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3344 2813 603 41 0 3303 0
vsize: 13376
[startup+390.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 2835 0 0 0 38991 9 0 0 25 0 1 0 481295848 13697024 2813 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3344 2813 603 41 0 3303 0
vsize: 13376
[startup+400.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 2835 0 0 0 39992 9 0 0 25 0 1 0 481295848 13697024 2813 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3344 2813 603 41 0 3303 0
vsize: 13376
[startup+410.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 2835 0 0 0 40992 9 0 0 25 0 1 0 481295848 13697024 2813 4294967295 134512640 134672761 3221224544 3221223648 134559927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3344 2813 603 41 0 3303 0
vsize: 13376
[startup+420.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 2835 0 0 0 41992 9 0 0 25 0 1 0 481295848 13697024 2813 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3344 2813 603 41 0 3303 0
vsize: 13376
[startup+430.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 2939 0 0 0 42991 10 0 0 25 0 1 0 481295848 14098432 2917 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3442 2917 603 41 0 3401 0
vsize: 13768
[startup+440.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 2968 0 0 0 43991 10 0 0 25 0 1 0 481295848 14233600 2946 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3475 2946 603 41 0 3434 0
vsize: 13900
[startup+450.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 2968 0 0 0 44991 10 0 0 25 0 1 0 481295848 14233600 2946 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3475 2946 603 41 0 3434 0
vsize: 13900
[startup+460.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 2976 0 0 0 45991 10 0 0 25 0 1 0 481295848 14233600 2954 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3475 2954 603 41 0 3434 0
vsize: 13900
[startup+470.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 3026 0 0 0 46991 10 0 0 25 0 1 0 481295848 14516224 3004 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3544 3004 603 41 0 3503 0
vsize: 14176
[startup+480.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 3102 0 0 0 47991 10 0 0 25 0 1 0 481295848 14925824 3080 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3644 3080 603 41 0 3603 0
vsize: 14576
[startup+490.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 3102 0 0 0 48992 10 0 0 25 0 1 0 481295848 14925824 3080 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3644 3080 603 41 0 3603 0
vsize: 14576
[startup+500.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 3117 0 0 0 49992 10 0 0 25 0 1 0 481295848 14925824 3095 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3644 3095 603 41 0 3603 0
vsize: 14576
[startup+510.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 3120 0 0 0 50992 10 0 0 25 0 1 0 481295848 14925824 3098 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3644 3098 603 41 0 3603 0
vsize: 14576
[startup+520.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 3120 0 0 0 51992 10 0 0 25 0 1 0 481295848 14925824 3098 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3644 3098 603 41 0 3603 0
vsize: 14576
[startup+530.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 3135 0 0 0 52992 10 0 0 25 0 1 0 481295848 15122432 3113 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3692 3113 603 41 0 3651 0
vsize: 14768
[startup+540.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 3146 0 0 0 53992 11 0 0 25 0 1 0 481295848 15122432 3124 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3692 3124 603 41 0 3651 0
vsize: 14768
[startup+550.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 3163 0 0 0 54992 11 0 0 25 0 1 0 481295848 15122432 3141 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3692 3141 603 41 0 3651 0
vsize: 14768
[startup+560.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 3163 0 0 0 55992 11 0 0 25 0 1 0 481295848 15122432 3141 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3692 3141 603 41 0 3651 0
vsize: 14768
[startup+570.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 3243 0 0 0 56992 11 0 0 25 0 1 0 481295848 15527936 3221 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3791 3221 603 41 0 3750 0
vsize: 15164
[startup+580.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 3400 0 0 0 57991 12 0 0 25 0 1 0 481295848 16203776 3378 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3956 3378 603 41 0 3915 0
vsize: 15824
[startup+590.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 3415 0 0 0 58991 12 0 0 25 0 1 0 481295848 16203776 3393 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3956 3393 603 41 0 3915 0
vsize: 15824
[startup+600.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 3416 0 0 0 59991 12 0 0 25 0 1 0 481295848 16203776 3394 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3956 3394 603 41 0 3915 0
vsize: 15824
[startup+610.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 3416 0 0 0 60992 12 0 0 25 0 1 0 481295848 16203776 3394 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3956 3394 603 41 0 3915 0
vsize: 15824
[startup+620.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 3454 0 0 0 61992 12 0 0 25 0 1 0 481295848 16338944 3432 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3989 3432 603 41 0 3948 0
vsize: 15956
[startup+630.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 3489 0 0 0 62992 12 0 0 25 0 1 0 481295848 16474112 3467 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4022 3467 603 41 0 3981 0
vsize: 16088
[startup+640.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 3506 0 0 0 63992 12 0 0 25 0 1 0 481295848 16609280 3484 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4055 3484 603 41 0 4014 0
vsize: 16220
[startup+650.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 3512 0 0 0 64992 12 0 0 25 0 1 0 481295848 16609280 3490 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4055 3490 603 41 0 4014 0
vsize: 16220
[startup+660.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 3520 0 0 0 65992 12 0 0 25 0 1 0 481295848 16609280 3498 4294967295 134512640 134672761 3221224544 3221223648 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4055 3498 603 41 0 4014 0
vsize: 16220
[startup+670.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 3533 0 0 0 66992 12 0 0 25 0 1 0 481295848 16773120 3511 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4095 3511 603 41 0 4054 0
vsize: 16380
[startup+680.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 3533 0 0 0 67992 12 0 0 25 0 1 0 481295848 16773120 3511 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4095 3511 603 41 0 4054 0
vsize: 16380
[startup+690.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 3535 0 0 0 68993 12 0 0 25 0 1 0 481295848 16773120 3513 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4095 3513 603 41 0 4054 0
vsize: 16380
[startup+700.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 3563 0 0 0 69993 12 0 0 25 0 1 0 481295848 16936960 3541 4294967295 134512640 134672761 3221224544 3221223648 134560303 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4135 3541 603 41 0 4094 0
vsize: 16540
[startup+710.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 3565 0 0 0 70993 12 0 0 25 0 1 0 481295848 16936960 3543 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4135 3543 603 41 0 4094 0
vsize: 16540
[startup+720.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 3617 0 0 0 71993 13 0 0 25 0 1 0 481295848 17072128 3595 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4168 3595 603 41 0 4127 0
vsize: 16672
[startup+730.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 3745 0 0 0 72993 13 0 0 25 0 1 0 481295848 17612800 3723 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4300 3723 603 41 0 4259 0
vsize: 17200
[startup+740.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 3762 0 0 0 73993 13 0 0 25 0 1 0 481295848 17747968 3740 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4333 3740 603 41 0 4292 0
vsize: 17332
[startup+750.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 3772 0 0 0 74993 13 0 0 25 0 1 0 481295848 17747968 3750 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4333 3750 603 41 0 4292 0
vsize: 17332
[startup+760.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 3787 0 0 0 75993 13 0 0 25 0 1 0 481295848 17891328 3765 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4368 3765 603 41 0 4327 0
vsize: 17472
[startup+770.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 3806 0 0 0 76993 13 0 0 25 0 1 0 481295848 18055168 3784 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4408 3784 603 41 0 4367 0
vsize: 17632
[startup+780.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 3824 0 0 0 77993 13 0 0 25 0 1 0 481295848 18055168 3802 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4408 3802 603 41 0 4367 0
vsize: 17632
[startup+790.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 3825 0 0 0 78994 13 0 0 25 0 1 0 481295848 18055168 3803 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4408 3803 603 41 0 4367 0
vsize: 17632
[startup+800.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 3832 0 0 0 79993 14 0 0 25 0 1 0 481295848 18055168 3810 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4408 3810 603 41 0 4367 0
vsize: 17632
[startup+810.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 3833 0 0 0 80993 14 0 0 25 0 1 0 481295848 18055168 3811 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4408 3811 603 41 0 4367 0
vsize: 17632
[startup+820.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 3864 0 0 0 81993 14 0 0 25 0 1 0 481295848 18219008 3842 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4448 3842 603 41 0 4407 0
vsize: 17792
[startup+830.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 3896 0 0 0 82993 14 0 0 25 0 1 0 481295848 18382848 3874 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4488 3874 603 41 0 4447 0
vsize: 17952
[startup+840.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 3897 0 0 0 83994 14 0 0 25 0 1 0 481295848 18382848 3875 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4488 3875 603 41 0 4447 0
vsize: 17952
[startup+850.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 3934 0 0 0 84994 14 0 0 25 0 1 0 481295848 18546688 3912 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4528 3912 603 41 0 4487 0
vsize: 18112
[startup+860.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 3934 0 0 0 85994 14 0 0 25 0 1 0 481295848 18546688 3912 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4528 3912 603 41 0 4487 0
vsize: 18112
[startup+870.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 3934 0 0 0 86994 14 0 0 25 0 1 0 481295848 18546688 3912 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4528 3912 603 41 0 4487 0
vsize: 18112
[startup+880.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 3957 0 0 0 87994 14 0 0 25 0 1 0 481295848 18681856 3935 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4561 3935 603 41 0 4520 0
vsize: 18244
[startup+890.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 4047 0 0 0 88994 14 0 0 25 0 1 0 481295848 19087360 4025 4294967295 134512640 134672761 3221224544 3221223680 134560654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4660 4025 603 41 0 4619 0
vsize: 18640
[startup+900.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 4053 0 0 0 89995 14 0 0 25 0 1 0 481295848 19087360 4031 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4660 4031 603 41 0 4619 0
vsize: 18640
[startup+910.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 4078 0 0 0 90995 14 0 0 25 0 1 0 481295848 19234816 4056 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4696 4056 603 41 0 4655 0
vsize: 18784
[startup+920.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 4101 0 0 0 91995 14 0 0 25 0 1 0 481295848 19398656 4079 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4736 4079 603 41 0 4695 0
vsize: 18944
[startup+930.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 4151 0 0 0 92995 14 0 0 25 0 1 0 481295848 19562496 4129 4294967295 134512640 134672761 3221224544 3221223648 134560212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4776 4129 603 41 0 4735 0
vsize: 19104
[startup+940.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 4159 0 0 0 93995 14 0 0 25 0 1 0 481295848 19562496 4137 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4776 4137 603 41 0 4735 0
vsize: 19104
[startup+950.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 4161 0 0 0 94995 14 0 0 25 0 1 0 481295848 19562496 4139 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4776 4139 603 41 0 4735 0
vsize: 19104
[startup+960.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 4161 0 0 0 95996 14 0 0 25 0 1 0 481295848 19562496 4139 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4776 4139 603 41 0 4735 0
vsize: 19104
[startup+970.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 4161 0 0 0 96996 14 0 0 25 0 1 0 481295848 19562496 4139 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4776 4139 603 41 0 4735 0
vsize: 19104
[startup+980.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 4162 0 0 0 97996 14 0 0 25 0 1 0 481295848 19562496 4140 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4776 4140 603 41 0 4735 0
vsize: 19104
[startup+990.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 4162 0 0 0 98996 14 0 0 25 0 1 0 481295848 19562496 4140 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4776 4140 603 41 0 4735 0
vsize: 19104
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 4164 0 0 0 99996 14 0 0 25 0 1 0 481295848 19562496 4142 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4776 4142 603 41 0 4735 0
vsize: 19104
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 4164 0 0 0 100996 14 0 0 25 0 1 0 481295848 19562496 4142 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4776 4142 603 41 0 4735 0
vsize: 19104
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 4203 0 0 0 101996 14 0 0 25 0 1 0 481295848 19890176 4181 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4856 4181 603 41 0 4815 0
vsize: 19424
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 4206 0 0 0 102997 14 0 0 25 0 1 0 481295848 19890176 4184 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4856 4184 603 41 0 4815 0
vsize: 19424
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 4215 0 0 0 103997 14 0 0 25 0 1 0 481295848 19890176 4193 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4856 4193 603 41 0 4815 0
vsize: 19424
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 4290 0 0 0 104997 14 0 0 25 0 1 0 481295848 20160512 4268 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4922 4268 603 41 0 4881 0
vsize: 19688
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 4315 0 0 0 105997 14 0 0 25 0 1 0 481295848 20299776 4293 4294967295 134512640 134672761 3221224544 3221223728 134558853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4956 4293 603 41 0 4915 0
vsize: 19824
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 4394 0 0 0 106997 15 0 0 25 0 1 0 481295848 20713472 4372 4294967295 134512640 134672761 3221224544 3221223728 134558360 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5057 4372 603 41 0 5016 0
vsize: 20228
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 4394 0 0 0 107997 15 0 0 25 0 1 0 481295848 20713472 4372 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5057 4372 603 41 0 5016 0
vsize: 20228
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 4394 0 0 0 108997 15 0 0 25 0 1 0 481295848 20692992 4372 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5052 4372 603 41 0 5011 0
vsize: 20208
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 4400 0 0 0 109997 15 0 0 25 0 1 0 481295848 20692992 4378 4294967295 134512640 134672761 3221224544 3221223712 134560954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5052 4378 603 41 0 5011 0
vsize: 20208
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 4419 0 0 0 110998 15 0 0 25 0 1 0 481295848 20692992 4397 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5052 4397 603 41 0 5011 0
vsize: 20208
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 4433 0 0 0 111998 15 0 0 25 0 1 0 481295848 20856832 4411 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5092 4411 603 41 0 5051 0
vsize: 20368
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 4433 0 0 0 112997 15 0 0 25 0 1 0 481295848 20856832 4411 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5092 4411 603 41 0 5051 0
vsize: 20368
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 4450 0 0 0 113998 15 0 0 25 0 1 0 481295848 20856832 4428 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5092 4428 603 41 0 5051 0
vsize: 20368
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 4466 0 0 0 114998 15 0 0 25 0 1 0 481295848 21020672 4444 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5132 4444 603 41 0 5091 0
vsize: 20528
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 4532 0 0 0 115998 15 0 0 25 0 1 0 481295848 21286912 4510 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5197 4510 603 41 0 5156 0
vsize: 20788
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 4532 0 0 0 116998 15 0 0 25 0 1 0 481295848 21286912 4510 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5197 4510 603 41 0 5156 0
vsize: 20788
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 4719 0 0 0 117997 16 0 0 25 0 1 0 481295848 22102016 4697 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5396 4697 603 41 0 5355 0
vsize: 21584
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 4746 0 0 0 118997 16 0 0 25 0 1 0 481295848 22249472 4724 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5432 4724 603 41 0 5391 0
vsize: 21728
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30815
Raw data (stat): 30815 (minisat+) R 30814 23176 23175 0 -1 0 4789 0 0 0 119997 16 0 0 25 0 1 0 481295848 22384640 4767 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5465 4767 603 41 0 5424 0
vsize: 21860
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 30815
Raw data (stat): 30815 (minisat+) Z 30814 23176 23175 0 -1 12 4791 0 0 0 119997 17 0 0 25 0 1 0 481295848 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.05
CPU time (s): 1200.16
CPU user time (s): 1199.98
CPU system time (s): 0.178972
CPU usage (%): 100.009
Max. virtual memory (Kb): 21860
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####