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-chnl20_30_pb.cnf.cr.opb
MD5SUMafcc4289aafaea265ed2d465965a3342
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 31
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.036993
Number of variables1200
Total number of constraints100
Number of constraints which are clauses60
Number of constraints which are cardinality constraints (but not clauses)40
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint20
Maximum length of a constraint30

Trace number 4746 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-04-13 20:09:56 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=86 boxname=wulflinc31 idbench=10 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  afcc4289aafaea265ed2d465965a3342  /oldhome/oroussel/tmp/wulflinc31/normalized-chnl20_30_pb.cnf.cr.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc31/normalized-chnl20_30_pb.cnf.cr.opb
IDLAUNCH: 86
/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:        912852 kB
Buffers:         34304 kB
Cached:          49080 kB
SwapCached:        392 kB
Active:          44740 kB
Inactive:        41848 kB
HighTotal:      131008 kB
HighFree:        78176 kB
LowTotal:       903652 kB
LowFree:        834676 kB
SwapTotal:     2097892 kB
SwapFree:      2097452 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6832 kB
Slab:            29588 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 20:29:58 (client local time) WITH STATUS 0 IN 1200.19 SECONDS
stats: 86 7 1200.19 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 100 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ............................................................
c ---[  39]---> BDD-cost:   57
c ---[  38]---> BDD-cost:   57
c ---[  37]---> BDD-cost:   57
c ---[  36]---> BDD-cost:   57
c ---[  35]---> BDD-cost:   57
c ---[  34]---> BDD-cost:   57
c ---[  33]---> BDD-cost:   57
c ---[  32]---> BDD-cost:   57
c ---[  31]---> BDD-cost:   57
c ---[  30]---> BDD-cost:   57
c ---[  29]---> BDD-cost:   57
c ---[  28]---> BDD-cost:   57
c ---[  27]---> BDD-cost:   57
c ---[  26]---> BDD-cost:   57
c ---[  25]---> BDD-cost:   57
c ---[  24]---> BDD-cost:   57
c ---[  23]---> BDD-cost:   57
c ---[  22]---> BDD-cost:   57
c ---[  21]---> BDD-cost:   57
c ---[  20]---> BDD-cost:   57
c ---[  19]---> BDD-cost:   57
c ---[  18]---> BDD-cost:   57
c ---[  17]---> BDD-cost:   57
c ---[  16]---> BDD-cost:   57
c ---[  15]---> BDD-cost:   57
c ---[  14]---> BDD-cost:   57
c ---[  13]---> BDD-cost:   57
c ---[  12]---> BDD-cost:   57
c ---[  11]---> BDD-cost:   57
c ---[  10]---> BDD-cost:   57
c ---[   9]---> BDD-cost:   57
c ---[   8]---> BDD-cost:   57
c ---[   7]---> BDD-cost:   57
c ---[   6]---> BDD-cost:   57
c ---[   5]---> BDD-cost:   57
c ---[   4]---> BDD-cost:   57
c ---[   3]---> BDD-cost:   57
c ---[   2]---> BDD-cost:   57
c ---[   1]---> BDD-cost:   57
c ---[   0]---> BDD-cost:   57
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    5700    15880 |    1900       0        0     nan |  0.000 % |
c |       100 |    5700    15880 |    2090     100     8350    83.5 |  1.149 % |
c |       254 |    5700    15880 |    2299     254    20183    79.5 |  1.149 % |
c |       483 |    5700    15880 |    2528     483    43595    90.3 |  1.150 % |
c |       820 |    5700    15880 |    2781     820    74636    91.0 |  1.149 % |
c |      1326 |    5700    15880 |    3059    1326   152844   115.3 |  1.149 % |
c |      2085 |    5700    15880 |    3365    2085   236742   113.5 |  1.149 % |
c |      3224 |    5700    15880 |    3702    3224   390616   121.2 |  1.149 % |
c |      4934 |    5700    15880 |    4072    2499   282510   113.0 |  1.149 % |
c |      7497 |    5700    15880 |    4480    5062   635699   125.6 |  1.149 % |
c |     11341 |    5700    15880 |    4928    3602   393130   109.1 |  1.149 % |
c |     17107 |    5700    15880 |    5420    3198   429474   134.3 |  1.149 % |
c |     25758 |    5700    15880 |    5963    5184   809083   156.1 |  1.149 % |
c |     38734 |    5700    15880 |    6559    4258   595019   139.7 |  1.149 % |
c |     58195 |    5700    15880 |    7215    4350   474363   109.0 |  1.149 % |
c |     87389 |    5700    15880 |    7936    5401   906885   167.9 |  1.149 % |
c |    131180 |    5700    15880 |    8730    8927  1807067   202.4 |  1.150 % |
c |    196867 |    5700    15880 |    9603    7833  1793666   229.0 |  1.149 % |
c |    295396 |    5700    15880 |   10563    5671   840337   148.2 |  1.149 % |
c |    443189 |    5700    15880 |   11620    8324  1522755   182.9 |  1.149 % |
c |    664881 |    5700    15880 |   12782    7923  1541577   194.6 |  1.149 % |
#### 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.90 2/54 25432
Raw data (stat): 25432 (runsolver) R 25431 23176 23175 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478708220 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 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.0003 s]
Raw data (loadavg): 0.93 0.97 0.90 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 1489 0 0 0 994 3 0 0 25 0 1 0 478708220 7593984 1467 4294967295 134512640 134672761 3221224624 3221223728 134554677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1854 1467 603 41 0 1813 0
vsize: 7416
[startup+20.0012 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 1799 0 0 0 1992 5 0 0 25 0 1 0 478708220 8957952 1777 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2187 1777 603 41 0 2146 0
vsize: 8748
[startup+30.0018 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 1929 0 0 0 2992 5 0 0 25 0 1 0 478708220 9490432 1907 4294967295 134512640 134672761 3221224624 3221223728 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2317 1907 603 41 0 2276 0
vsize: 9268
[startup+40.0022 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 2072 0 0 0 3991 5 0 0 25 0 1 0 478708220 10031104 2050 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2449 2050 603 41 0 2408 0
vsize: 9796
[startup+50.003 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 2097 0 0 0 4991 6 0 0 25 0 1 0 478708220 10178560 2075 4294967295 134512640 134672761 3221224624 3221223728 134560002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2485 2075 603 41 0 2444 0
vsize: 9940
[startup+60.0032 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 2131 0 0 0 5991 6 0 0 25 0 1 0 478708220 10326016 2109 4294967295 134512640 134672761 3221224624 3221223728 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2521 2109 603 41 0 2480 0
vsize: 10084
[startup+70.0039 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 2338 0 0 0 6991 6 0 0 25 0 1 0 478708220 11280384 2316 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2754 2316 603 41 0 2713 0
vsize: 11016
[startup+80.0038 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 2511 0 0 0 7990 7 0 0 25 0 1 0 478708220 11956224 2489 4294967295 134512640 134672761 3221224624 3221223808 134558851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2919 2489 603 41 0 2878 0
vsize: 11676
[startup+90.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 2607 0 0 0 8990 8 0 0 25 0 1 0 478708220 12369920 2585 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3020 2585 603 41 0 2979 0
vsize: 12080
[startup+100.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 2926 0 0 0 9989 9 0 0 25 0 1 0 478708220 13713408 2904 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3348 2904 603 41 0 3307 0
vsize: 13392
[startup+110.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 2976 0 0 0 10989 9 0 0 25 0 1 0 478708220 13852672 2954 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3382 2954 603 41 0 3341 0
vsize: 13528
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 3051 0 0 0 11989 9 0 0 25 0 1 0 478708220 14258176 3029 4294967295 134512640 134672761 3221224624 3221223808 134558875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3481 3029 603 41 0 3440 0
vsize: 13924
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 3051 0 0 0 12989 9 0 0 25 0 1 0 478708220 14258176 3029 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3481 3029 603 41 0 3440 0
vsize: 13924
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 3297 0 0 0 13989 9 0 0 25 0 1 0 478708220 15200256 3275 4294967295 134512640 134672761 3221224624 3221223728 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3711 3275 603 41 0 3670 0
vsize: 14844
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 3436 0 0 0 14989 10 0 0 25 0 1 0 478708220 15753216 3414 4294967295 134512640 134672761 3221224624 3221223808 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3846 3414 603 41 0 3805 0
vsize: 15384
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 3674 0 0 0 15988 10 0 0 25 0 1 0 478708220 16834560 3652 4294967295 134512640 134672761 3221224624 3221223808 134559622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4110 3652 603 41 0 4069 0
vsize: 16440
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 3898 0 0 0 16988 11 0 0 25 0 1 0 478708220 17780736 3876 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4341 3876 603 41 0 4300 0
vsize: 17364
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4031 0 0 0 17988 11 0 0 25 0 1 0 478708220 18321408 4009 4294967295 134512640 134672761 3221224624 3221223728 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4473 4009 603 41 0 4432 0
vsize: 17892
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4055 0 0 0 18988 11 0 0 25 0 1 0 478708220 18321408 4033 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4473 4033 603 41 0 4432 0
vsize: 17892
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4055 0 0 0 19988 11 0 0 25 0 1 0 478708220 18321408 4033 4294967295 134512640 134672761 3221224624 3221223808 134558761 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4473 4033 603 41 0 4432 0
vsize: 17892
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4068 0 0 0 20988 11 0 0 25 0 1 0 478708220 18481152 4046 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4512 4046 603 41 0 4471 0
vsize: 18048
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4079 0 0 0 21988 11 0 0 25 0 1 0 478708220 18481152 4057 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4512 4057 603 41 0 4471 0
vsize: 18048
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4080 0 0 0 22989 11 0 0 25 0 1 0 478708220 18481152 4058 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4512 4058 603 41 0 4471 0
vsize: 18048
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4238 0 0 0 23988 12 0 0 25 0 1 0 478708220 19152896 4216 4294967295 134512640 134672761 3221224624 3221223728 134559887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4676 4216 603 41 0 4635 0
vsize: 18704
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4264 0 0 0 24988 12 0 0 25 0 1 0 478708220 19288064 4242 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4709 4242 603 41 0 4668 0
vsize: 18836
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4408 0 0 0 25988 12 0 0 25 0 1 0 478708220 19963904 4386 4294967295 134512640 134672761 3221224624 3221223728 134560424 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4874 4386 603 41 0 4833 0
vsize: 19496
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4415 0 0 0 26988 12 0 0 25 0 1 0 478708220 19963904 4393 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4874 4393 603 41 0 4833 0
vsize: 19496
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4416 0 0 0 27988 12 0 0 25 0 1 0 478708220 19963904 4394 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4874 4394 603 41 0 4833 0
vsize: 19496
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4416 0 0 0 28988 12 0 0 25 0 1 0 478708220 19963904 4394 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4874 4394 603 41 0 4833 0
vsize: 19496
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4416 0 0 0 29988 12 0 0 25 0 1 0 478708220 19963904 4394 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4874 4394 603 41 0 4833 0
vsize: 19496
[startup+310.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4417 0 0 0 30988 12 0 0 25 0 1 0 478708220 19963904 4395 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4874 4395 603 41 0 4833 0
vsize: 19496
[startup+320.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4418 0 0 0 31989 12 0 0 25 0 1 0 478708220 19963904 4396 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4874 4396 603 41 0 4833 0
vsize: 19496
[startup+330.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4418 0 0 0 32989 12 0 0 25 0 1 0 478708220 19963904 4396 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4874 4396 603 41 0 4833 0
vsize: 19496
[startup+340.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4418 0 0 0 33989 12 0 0 25 0 1 0 478708220 19963904 4396 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4874 4396 603 41 0 4833 0
vsize: 19496
[startup+350.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4418 0 0 0 34989 12 0 0 25 0 1 0 478708220 19963904 4396 4294967295 134512640 134672761 3221224624 3221223808 134558332 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4874 4396 603 41 0 4833 0
vsize: 19496
[startup+360.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4418 0 0 0 35989 12 0 0 25 0 1 0 478708220 19963904 4396 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4874 4396 603 41 0 4833 0
vsize: 19496
[startup+370.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4418 0 0 0 36990 12 0 0 25 0 1 0 478708220 19963904 4396 4294967295 134512640 134672761 3221224624 3221223728 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4874 4396 603 41 0 4833 0
vsize: 19496
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4418 0 0 0 37990 12 0 0 25 0 1 0 478708220 19963904 4396 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4874 4396 603 41 0 4833 0
vsize: 19496
[startup+390.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4418 0 0 0 38990 12 0 0 25 0 1 0 478708220 19963904 4396 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4874 4396 603 41 0 4833 0
vsize: 19496
[startup+400.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4418 0 0 0 39990 12 0 0 25 0 1 0 478708220 19963904 4396 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4874 4396 603 41 0 4833 0
vsize: 19496
[startup+410.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4418 0 0 0 40990 12 0 0 25 0 1 0 478708220 19963904 4396 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4874 4396 603 41 0 4833 0
vsize: 19496
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4418 0 0 0 41991 12 0 0 25 0 1 0 478708220 19963904 4396 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4874 4396 603 41 0 4833 0
vsize: 19496
[startup+430.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4418 0 0 0 42991 12 0 0 25 0 1 0 478708220 19963904 4396 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4874 4396 603 41 0 4833 0
vsize: 19496
[startup+440.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4418 0 0 0 43990 12 0 0 25 0 1 0 478708220 19963904 4396 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4874 4396 603 41 0 4833 0
vsize: 19496
[startup+450.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4419 0 0 0 44990 13 0 0 25 0 1 0 478708220 19963904 4397 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4874 4397 603 41 0 4833 0
vsize: 19496
[startup+460.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4420 0 0 0 45991 13 0 0 25 0 1 0 478708220 19963904 4398 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4874 4398 603 41 0 4833 0
vsize: 19496
[startup+470.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4420 0 0 0 46991 13 0 0 25 0 1 0 478708220 19963904 4398 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4874 4398 603 41 0 4833 0
vsize: 19496
[startup+480.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4420 0 0 0 47991 13 0 0 25 0 1 0 478708220 19963904 4398 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4874 4398 603 41 0 4833 0
vsize: 19496
[startup+490.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4420 0 0 0 48991 13 0 0 25 0 1 0 478708220 19963904 4398 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4874 4398 603 41 0 4833 0
vsize: 19496
[startup+500.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4420 0 0 0 49991 13 0 0 25 0 1 0 478708220 19963904 4398 4294967295 134512640 134672761 3221224624 3221223792 134561003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4874 4398 603 41 0 4833 0
vsize: 19496
[startup+510.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4420 0 0 0 50991 13 0 0 25 0 1 0 478708220 19963904 4398 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4874 4398 603 41 0 4833 0
vsize: 19496
[startup+520.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4479 0 0 0 51992 13 0 0 25 0 1 0 478708220 20234240 4457 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4940 4457 603 41 0 4899 0
vsize: 19760
[startup+530.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4480 0 0 0 52992 13 0 0 25 0 1 0 478708220 20234240 4458 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4940 4458 603 41 0 4899 0
vsize: 19760
[startup+540.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4480 0 0 0 53992 13 0 0 25 0 1 0 478708220 20234240 4458 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4940 4458 603 41 0 4899 0
vsize: 19760
[startup+550.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4480 0 0 0 54992 13 0 0 25 0 1 0 478708220 20230144 4458 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4939 4458 603 41 0 4898 0
vsize: 19756
[startup+560.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4480 0 0 0 55992 13 0 0 25 0 1 0 478708220 20230144 4458 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4939 4458 603 41 0 4898 0
vsize: 19756
[startup+570.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4488 0 0 0 56992 13 0 0 25 0 1 0 478708220 20230144 4466 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4939 4466 603 41 0 4898 0
vsize: 19756
[startup+580.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4488 0 0 0 57992 13 0 0 25 0 1 0 478708220 20230144 4466 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4939 4466 603 41 0 4898 0
vsize: 19756
[startup+590.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4494 0 0 0 58993 13 0 0 25 0 1 0 478708220 20230144 4472 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4939 4472 603 41 0 4898 0
vsize: 19756
[startup+600.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4495 0 0 0 59993 13 0 0 25 0 1 0 478708220 20230144 4473 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4939 4473 603 41 0 4898 0
vsize: 19756
[startup+610.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4495 0 0 0 60993 13 0 0 25 0 1 0 478708220 20230144 4473 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4939 4473 603 41 0 4898 0
vsize: 19756
[startup+620.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4546 0 0 0 61993 13 0 0 25 0 1 0 478708220 20496384 4524 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5004 4524 603 41 0 4963 0
vsize: 20016
[startup+630.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4610 0 0 0 62993 13 0 0 25 0 1 0 478708220 20770816 4588 4294967295 134512640 134672761 3221224624 3221223808 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5071 4588 603 41 0 5030 0
vsize: 20284
[startup+640.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4622 0 0 0 63993 13 0 0 25 0 1 0 478708220 20770816 4600 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5071 4600 603 41 0 5030 0
vsize: 20284
[startup+650.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4623 0 0 0 64994 13 0 0 25 0 1 0 478708220 20770816 4601 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5071 4601 603 41 0 5030 0
vsize: 20284
[startup+660.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4623 0 0 0 65994 13 0 0 25 0 1 0 478708220 20770816 4601 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5071 4601 603 41 0 5030 0
vsize: 20284
[startup+670.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4623 0 0 0 66994 13 0 0 25 0 1 0 478708220 20770816 4601 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5071 4601 603 41 0 5030 0
vsize: 20284
[startup+680.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4735 0 0 0 67994 13 0 0 25 0 1 0 478708220 21315584 4713 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5204 4713 603 41 0 5163 0
vsize: 20816
[startup+690.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4750 0 0 0 68994 14 0 0 25 0 1 0 478708220 21315584 4728 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5204 4728 603 41 0 5163 0
vsize: 20816
[startup+700.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4750 0 0 0 69994 14 0 0 25 0 1 0 478708220 21315584 4728 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5204 4728 603 41 0 5163 0
vsize: 20816
[startup+710.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4856 0 0 0 70994 14 0 0 25 0 1 0 478708220 21856256 4834 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5336 4834 603 41 0 5295 0
vsize: 21344
[startup+720.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4858 0 0 0 71994 14 0 0 25 0 1 0 478708220 21856256 4836 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5336 4836 603 41 0 5295 0
vsize: 21344
[startup+730.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4858 0 0 0 72994 14 0 0 25 0 1 0 478708220 21856256 4836 4294967295 134512640 134672761 3221224624 3221223640 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5336 4836 603 41 0 5295 0
vsize: 21344
[startup+740.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4864 0 0 0 73994 14 0 0 25 0 1 0 478708220 21856256 4842 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5336 4842 603 41 0 5295 0
vsize: 21344
[startup+750.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4864 0 0 0 74994 14 0 0 25 0 1 0 478708220 21856256 4842 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5336 4842 603 41 0 5295 0
vsize: 21344
[startup+760.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4884 0 0 0 75994 14 0 0 25 0 1 0 478708220 21995520 4862 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5370 4862 603 41 0 5329 0
vsize: 21480
[startup+770.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4885 0 0 0 76994 14 0 0 25 0 1 0 478708220 21995520 4863 4294967295 134512640 134672761 3221224624 3221223776 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5370 4863 603 41 0 5329 0
vsize: 21480
[startup+780.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4890 0 0 0 77994 14 0 0 25 0 1 0 478708220 21995520 4868 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5370 4868 603 41 0 5329 0
vsize: 21480
[startup+790.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4890 0 0 0 78995 14 0 0 25 0 1 0 478708220 21995520 4868 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5370 4868 603 41 0 5329 0
vsize: 21480
[startup+800.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4890 0 0 0 79995 14 0 0 25 0 1 0 478708220 21995520 4868 4294967295 134512640 134672761 3221224624 3221223808 134559581 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5370 4868 603 41 0 5329 0
vsize: 21480
[startup+810.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4890 0 0 0 80995 14 0 0 25 0 1 0 478708220 21995520 4868 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5370 4868 603 41 0 5329 0
vsize: 21480
[startup+820.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4891 0 0 0 81995 14 0 0 25 0 1 0 478708220 21995520 4869 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5370 4869 603 41 0 5329 0
vsize: 21480
[startup+830.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4892 0 0 0 82995 14 0 0 25 0 1 0 478708220 21995520 4870 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5370 4870 603 41 0 5329 0
vsize: 21480
[startup+840.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4892 0 0 0 83996 14 0 0 25 0 1 0 478708220 21995520 4870 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5370 4870 603 41 0 5329 0
vsize: 21480
[startup+850.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4901 0 0 0 84996 14 0 0 25 0 1 0 478708220 21995520 4879 4294967295 134512640 134672761 3221224624 3221223792 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5370 4879 603 41 0 5329 0
vsize: 21480
[startup+860.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4902 0 0 0 85996 14 0 0 25 0 1 0 478708220 21995520 4880 4294967295 134512640 134672761 3221224624 3221223728 134560136 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5370 4880 603 41 0 5329 0
vsize: 21480
[startup+870.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4902 0 0 0 86996 14 0 0 25 0 1 0 478708220 21995520 4880 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5370 4880 603 41 0 5329 0
vsize: 21480
[startup+880.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 4993 0 0 0 87996 14 0 0 25 0 1 0 478708220 22401024 4971 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5469 4971 603 41 0 5428 0
vsize: 21876
[startup+890.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 5067 0 0 0 88996 15 0 0 25 0 1 0 478708220 22810624 5045 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5569 5045 603 41 0 5528 0
vsize: 22276
[startup+900.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 5099 0 0 0 89996 15 0 0 25 0 1 0 478708220 22974464 5077 4294967295 134512640 134672761 3221224624 3221223728 134555105 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5609 5077 603 41 0 5568 0
vsize: 22436
[startup+910.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 5113 0 0 0 90997 15 0 0 25 0 1 0 478708220 22974464 5091 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5609 5091 603 41 0 5568 0
vsize: 22436
[startup+920.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 5140 0 0 0 91997 15 0 0 25 0 1 0 478708220 23126016 5118 4294967295 134512640 134672761 3221224624 3221223808 134558851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5646 5118 603 41 0 5605 0
vsize: 22584
[startup+930.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 5151 0 0 0 92997 15 0 0 25 0 1 0 478708220 23289856 5129 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5686 5129 603 41 0 5645 0
vsize: 22744
[startup+940.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 5151 0 0 0 93997 15 0 0 25 0 1 0 478708220 23289856 5129 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5686 5129 603 41 0 5645 0
vsize: 22744
[startup+950.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 5152 0 0 0 94997 15 0 0 25 0 1 0 478708220 23289856 5130 4294967295 134512640 134672761 3221224624 3221223808 134559385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5686 5130 603 41 0 5645 0
vsize: 22744
[startup+960.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 5174 0 0 0 95997 15 0 0 25 0 1 0 478708220 23289856 5152 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5686 5152 603 41 0 5645 0
vsize: 22744
[startup+970.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 5253 0 0 0 96997 15 0 0 25 0 1 0 478708220 23691264 5231 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5784 5231 603 41 0 5743 0
vsize: 23136
[startup+980.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 5393 0 0 0 97997 15 0 0 25 0 1 0 478708220 24231936 5371 4294967295 134512640 134672761 3221224624 3221223808 134559334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5916 5371 603 41 0 5875 0
vsize: 23664
[startup+990.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 5393 0 0 0 98997 15 0 0 25 0 1 0 478708220 24231936 5371 4294967295 134512640 134672761 3221224624 3221223800 134558780 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5916 5371 603 41 0 5875 0
vsize: 23664
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 5394 0 0 0 99998 15 0 0 25 0 1 0 478708220 24231936 5372 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5916 5372 603 41 0 5875 0
vsize: 23664
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 5475 0 0 0 100998 15 0 0 25 0 1 0 478708220 24502272 5453 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5982 5453 603 41 0 5941 0
vsize: 23928
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 5494 0 0 0 101998 15 0 0 25 0 1 0 478708220 24637440 5472 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6015 5472 603 41 0 5974 0
vsize: 24060
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 5787 0 0 0 102998 16 0 0 25 0 1 0 478708220 25845760 5765 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6310 5765 603 41 0 6269 0
vsize: 25240
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 6073 0 0 0 103997 16 0 0 25 0 1 0 478708220 26939392 6051 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6577 6051 603 41 0 6536 0
vsize: 26308
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 6073 0 0 0 104998 16 0 0 25 0 1 0 478708220 26939392 6051 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6577 6051 603 41 0 6536 0
vsize: 26308
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 6073 0 0 0 105998 16 0 0 25 0 1 0 478708220 26939392 6051 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6577 6051 603 41 0 6536 0
vsize: 26308
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 6073 0 0 0 106998 16 0 0 25 0 1 0 478708220 26939392 6051 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6577 6051 603 41 0 6536 0
vsize: 26308
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 6074 0 0 0 107998 16 0 0 25 0 1 0 478708220 26939392 6052 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6577 6052 603 41 0 6536 0
vsize: 26308
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 6074 0 0 0 108998 16 0 0 25 0 1 0 478708220 26939392 6052 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6577 6052 603 41 0 6536 0
vsize: 26308
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 6075 0 0 0 109998 17 0 0 25 0 1 0 478708220 26939392 6053 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6577 6053 603 41 0 6536 0
vsize: 26308
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 6076 0 0 0 110998 17 0 0 25 0 1 0 478708220 26939392 6054 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6577 6054 603 41 0 6536 0
vsize: 26308
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 6076 0 0 0 111998 17 0 0 25 0 1 0 478708220 26939392 6054 4294967295 134512640 134672761 3221224624 3221223808 134559604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6577 6054 603 41 0 6536 0
vsize: 26308
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 6076 0 0 0 112998 17 0 0 25 0 1 0 478708220 26939392 6054 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6577 6054 603 41 0 6536 0
vsize: 26308
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 6076 0 0 0 113999 17 0 0 25 0 1 0 478708220 26939392 6054 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6577 6054 603 41 0 6536 0
vsize: 26308
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 6076 0 0 0 114999 17 0 0 25 0 1 0 478708220 26939392 6054 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6577 6054 603 41 0 6536 0
vsize: 26308
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 6076 0 0 0 115999 17 0 0 25 0 1 0 478708220 26939392 6054 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6577 6054 603 41 0 6536 0
vsize: 26308
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 6078 0 0 0 116999 17 0 0 25 0 1 0 478708220 26939392 6056 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6577 6056 603 41 0 6536 0
vsize: 26308
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 6084 0 0 0 117999 17 0 0 25 0 1 0 478708220 27119616 6062 4294967295 134512640 134672761 3221224624 3221223776 134565064 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6621 6062 603 41 0 6580 0
vsize: 26484
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 6084 0 0 0 119000 17 0 0 25 0 1 0 478708220 27119616 6062 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6621 6062 603 41 0 6580 0
vsize: 26484
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25432
Raw data (stat): 25432 (minisat+) R 25431 23176 23175 0 -1 0 6084 0 0 0 120000 17 0 0 25 0 1 0 478708220 27119616 6062 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6621 6062 603 41 0 6580 0
vsize: 26484
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 25432
Raw data (stat): 25432 (minisat+) Z 25431 23176 23175 0 -1 12 6086 0 0 0 120000 18 0 0 25 0 1 0 478708220 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.06
CPU time (s): 1200.19
CPU user time (s): 1200
CPU system time (s): 0.186971
CPU usage (%): 100.011
Max. virtual memory (Kb): 26484
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####