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).
    Note that some very long lines in this section may be truncated by your web browser !
  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

Namemps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-d6cube.opb
MD5SUM889599bea53ff906bd4dd516c552c027
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
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 123680
Biggest coefficient in the objective function 524288
Number of bits for the biggest coefficient in the objective function 20
Sum of the numbers in the objective function 6484387800
Number of bits of the sum of numbers in the objective function 33
Biggest number in a constraint 188743680
Number of bits of the biggest number in a constraint 28
Biggest sum of numbers in a constraint 10767194085
Number of bits of the biggest sum of numbers34
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark28.7566
Number of variables123680
Total number of constraints404
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints404
Minimum length of a constraint20
Maximum length of a constraint123680

Trace number 6004

Launcher Data

LAUNCH ON wulflinc22 THE 2005-09-20 02:35:17 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3149 boxname=wulflinc22 idbench=805 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  889599bea53ff906bd4dd516c552c027  /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-d6cube.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-d6cube.opb
IDLAUNCH: 3149
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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	: 890.88

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        890008 kB
Buffers:          1796 kB
Cached:         115564 kB
SwapCached:        484 kB
Active:          29368 kB
Inactive:        90424 kB
HighTotal:      131008 kB
HighFree:        11872 kB
LowTotal:       903652 kB
LowFree:        878136 kB
SwapTotal:     2097892 kB
SwapFree:      2096748 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5676 kB
Slab:            18996 kB
Committed_AS:    64132 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 02:55:28 (client local time) WITH STATUS 0 IN 1202.14 SECONDS
stats: 3149 7 1202.14 0

Solver Data

c Parsing PB file...
c Converting 808 PB-constraints to clauses...
c   -- Unit propagations: pppp
c   -- Detecting intervals from adjacent constraints: ###################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 806]---> Adder-cost: 1066   maxlim: 2752486   bits: 22/22
c ---[ 804]---> Sorter-cost: 1184     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 802]---> Adder-cost: 782   maxlim: 1376234   bits: 21/21
c ---[ 800]---> Adder-cost: 482   maxlim: 688118   bits: 21/20
c ---[ 798]---> Adder-cost: 1006   maxlim: 1867753   bits: 22/21
c ---[ 796]---> Adder-cost: 614   maxlim: 1048562   bits: 21/20
c ---[ 794]---> Adder-cost: 970   maxlim: 1867753   bits: 22/21
c ---[ 792]---> Adder-cost: 1336   maxlim: 2621408   bits: 22/22
c ---[ 790]---> Adder-cost: 1396   maxlim: 2654175   bits: 22/22
c ---[ 788]---> Adder-cost: 1366   maxlim: 2654175   bits: 22/22
c ---[ 786]---> Adder-cost: 920   maxlim: 2031594   bits: 22/21
c ---[ 784]---> Adder-cost: 1010   maxlim: 1834986   bits: 22/21
c ---[ 782]---> Adder-cost: 1004   maxlim: 1900520   bits: 22/21
c ---[ 780]---> Adder-cost: 1366   maxlim: 2686942   bits: 22/22
c ---[ 778]---> Adder-cost: 552   maxlim: 1146868   bits: 21/21
c ---[ 776]---> Adder-cost: 948   maxlim: 1802219   bits: 22/21
c ---[ 774]---> Adder-cost: 1538   maxlim: 2293734   bits: 23/22
c ---[ 772]---> Adder-cost: 1537   maxlim: 2293734   bits: 23/22
c ---[ 770]---> Adder-cost: 644   maxlim: 1114096   bits: 21/21
c ---[ 768]---> Adder-cost: 1062   maxlim: 1933285   bits: 22/21
c ---[ 766]---> Adder-cost: 1092   maxlim: 1900518   bits: 22/21
c ---[ 764]---> Adder-cost: 644   maxlim: 1179631   bits: 21/21
c ---[ 762]---> Adder-cost: 1017   maxlim: 1048558   bits: 21/20
c ---[ 760]---> Adder-cost: 1184   maxlim: 1277932   bits: 22/21
c ---[ 758]---> Adder-cost: 730   maxlim: 688116   bits: 21/20
c ---[ 756]---> Adder-cost: 934   maxlim: 1179631   bits: 22/21
c ---[ 754]---> Adder-cost: 310   maxlim: 393208   bits: 20/19
c ---[ 752]---> Adder-cost: 602   maxlim: 786420   bits: 21/20
c ---[ 750]---> Adder-cost: 934   maxlim: 1441774   bits: 22/21
c ---[ 748]---> Adder-cost: 348   maxlim: 491512   bits: 20/19
c ---[ 746]---> Adder-cost: 332   maxlim: 393206   bits: 19/19
c ---[ 744]---> Adder-cost: 810   maxlim: 1392621   bits: 22/21
c ---[ 742]---> Adder-cost: 902   maxlim: 1638378   bits: 22/21
c ---[ 740]---> Adder-cost: 902   maxlim: 1638378   bits: 22/21
c ---[ 738]---> Adder-cost: 1446   maxlim: 2850777   bits: 22/22
c ---[ 736]---> Adder-cost: 1022   maxlim: 1245164   bits: 22/21
c ---[ 734]---> Adder-cost: 578   maxlim: 524280   bits: 20/19
c ---[ 732]---> Adder-cost: 798   maxlim: 851955   bits: 21/20
c ---[ 730]---> Adder-cost: 1288   maxlim: 1572840   bits: 22/21
c ---[ 728]---> Adder-cost: 1286   maxlim: 1507306   bits: 22/21
c ---[ 726]---> Adder-cost: 948   maxlim: 1441778   bits: 22/21
c ---[ 724]---> Adder-cost: 1022   maxlim: 1179630   bits: 22/21
c ---[ 722]---> Adder-cost: 1286   maxlim: 1474539   bits: 22/21
c ---[ 720]---> Adder-cost: 949   maxlim: 1015797   bits: 21/20
c ---[ 718]---> Adder-cost: 749   maxlim: 819190   bits: 21/20
c ---[ 716]---> Adder-cost: 473   maxlim: 393209   bits: 20/19
c ---[ 714]---> Adder-cost: 905   maxlim: 1015793   bits: 21/20
c ---[ 712]---> Adder-cost: 1106   maxlim: 1900514   bits: 22/21
c ---[ 710]---> Adder-cost: 924   maxlim: 1572839   bits: 22/21
c ---[ 708]---> Adder-cost: 1410   maxlim: 2113505   bits: 22/22
c ---[ 706]---> Adder-cost: 1350   maxlim: 1982437   bits: 22/21
c ---[ 704]---> Adder-cost: 1408   maxlim: 2080738   bits: 22/21
c ---[ 702]---> Adder-cost: 1318   maxlim: 1966054   bits: 22/21
c ---[ 700]---> Adder-cost: 908   maxlim: 1409007   bits: 22/21
c ---[ 698]---> Adder-cost: 798   maxlim: 1146865   bits: 21/21
c ---[ 696]---> Adder-cost: 734   maxlim: 1114097   bits: 21/21
c ---[ 694]---> Adder-cost: 1260   maxlim: 1933287   bits: 22/21
c ---[ 692]---> Adder-cost: 836   maxlim: 1245166   bits: 22/21
c ---[ 690]---> Adder-cost: 1066   maxlim: 2949093   bits: 22/22
c ---[ 688]---> Adder-cost: 1080   maxlim: 1523688   bits: 22/21
c ---[ 686]---> Adder-cost: 886   maxlim: 1261549   bits: 21/21
c ---[ 684]---> Adder-cost: 748   maxlim: 540659   bits: 21/20
c ---[ 682]---> Adder-cost: 724   maxlim: 475126   bits: 20/19
c ---[ 680]---> Adder-cost: 659   maxlim: 442358   bits: 20/19
c ---[ 678]---> Adder-cost: 406   maxlim: 376825   bits: 20/19
c ---[ 676]---> Adder-cost: 520   maxlim: 688114   bits: 20/20
c ---[ 674]---> Adder-cost: 1037   maxlim: 884718   bits: 21/20
c ---[ 672]---> Adder-cost: 698   maxlim: 458744   bits: 20/19
c ---[ 670]---> Adder-cost: 1143   maxlim: 851953   bits: 21/20
c ---[ 668]---> Adder-cost: 533   maxlim: 360440   bits: 20/19
c ---[ 666]---> Adder-cost: 730   maxlim: 491511   bits: 20/19
c ---[ 664]---> Adder-cost: 1064   maxlim: 3145698   bits: 22/22
c ---[ 662]---> Adder-cost: 978   maxlim: 1196013   bits: 22/21
c ---[ 660]---> Adder-cost: 1334   maxlim: 1654758   bits: 22/21
c ---[ 658]---> Adder-cost: 896   maxlim: 1081329   bits: 22/21
c ---[ 656]---> Adder-cost: 630   maxlim: 770035   bits: 21/20
c ---[ 654]---> Adder-cost: 396   maxlim: 131066   bits: 18/17
c ---[ 652]---> Adder-cost: 426   maxlim: 442357   bits: 20/19
c ---[ 650]---> Adder-cost: 796   maxlim: 1228782   bits: 21/21
c ---[ 648]---> Adder-cost: 1052   maxlim: 1753062   bits: 22/21
c ---[ 646]---> Adder-cost: 766   maxlim: 1228782   bits: 21/21
c ---[ 644]---> Adder-cost: 704   maxlim: 409594   bits: 20/19
c ---[ 642]---> Adder-cost: 1300   maxlim: 1196011   bits: 22/21
c ---[ 640]---> Adder-cost: 631   maxlim: 475127   bits: 20/19
c ---[ 638]---> Adder-cost: 1085   maxlim: 901106   bits: 21/20
c ---[ 636]---> Adder-cost: 1360   maxlim: 1261546   bits: 22/21
c ---[ 634]---> Adder-cost: 1208   maxlim: 1130476   bits: 22/21
c ---[ 632]---> Adder-cost: 959   maxlim: 770037   bits: 21/20
c ---[ 630]---> Adder-cost: 756   maxlim: 540661   bits: 21/20
c ---[ 628]---> Adder-cost: 758   maxlim: 638964   bits: 21/20
c ---[ 626]---> Adder-cost: 333   maxlim: 114682   bits: 18/17
c ---[ 624]---> Adder-cost: 1068   maxlim: 1589222   bits: 22/21
c ---[ 622]---> Adder-cost: 730   maxlim: 835571   bits: 21/20
c ---[ 620]---> Adder-cost: 542   maxlim: 704503   bits: 21/20
c ---[ 618]---> Adder-cost: 978   maxlim: 1245165   bits: 22/21
c ---[ 616]---> Adder-cost: 898   maxlim: 1196015   bits: 22/21
c ---[ 614]---> Adder-cost: 838   maxlim: 1146986   bits: 21/21
c ---[ 612]---> Adder-cost: 1068   maxlim: 1327210   bits: 22/21
c ---[ 610]---> Adder-cost: 1010   maxlim: 1310826   bits: 22/21
c ---[ 608]---> Adder-cost: 971   maxlim: 491508   bits: 20/19
c ---[ 606]---> Adder-cost: 1305   maxlim: 884716   bits: 21/20
c ---[ 604]---> Adder-cost: 874   maxlim: 507892   bits: 20/19
c ---[ 602]---> Adder-cost: 655   maxlim: 344055   bits: 20/19
c ---[ 600]---> Adder-cost: 774   maxlim: 917487   bits: 21/20
c ---[ 598]---> Adder-cost: 722   maxlim: 786547   bits: 21/20
c ---[ 596]---> Adder-cost: 1264   maxlim: 1474538   bits: 22/21
c ---[ 594]---> Adder-cost: 602   maxlim: 163832   bits: 19/18
c ---[ 592]---> Adder-cost: 870   maxlim: 770034   bits: 21/20
c ---[ 590]---> Adder-cost: 844   maxlim: 491509   bits: 20/19
c ---[ 588]---> Adder-cost: 653   maxlim: 425974   bits: 20/19
c ---[ 586]---> Adder-cost: 859   maxlim: 458868   bits: 20/19
c ---[ 584]---> Adder-cost: 739   maxlim: 360566   bits: 20/19
c ---[ 582]---> Adder-cost: 1096   maxlim: 3080163   bits: 22/22
c ---[ 580]---> Adder-cost: 759   maxlim: 196599   bits: 19/18
c ---[ 578]---> Adder-cost: 214792   maxlim: 783178288   bits: 30/30
c ---[ 576]---> Adder-cost: 125388   maxlim: 586954496   bits: 30/30
c ---[ 574]---> Adder-cost: 76899   maxlim: 488500119   bits: 29/29
c ---[ 572]---> Adder-cost: 60290   maxlim: 571647874   bits: 30/30
c ---[ 570]---> Adder-cost: 65668   maxlim: 921819109   bits: 30/30
c ---[ 566]---> Adder-cost: 1038   maxlim: 2752488   bits: 22/22
c ---[ 564]---> Adder-cost: 1070   maxlim: 2818023   bits: 22/22
c ---[ 562]---> Adder-cost: 698   maxlim: 983023   bits: 21/20
c ---[ 560]---> Adder-cost: 756   maxlim: 1114091   bits: 21/21
c ---[ 558]---> Adder-cost: 698   maxlim: 983023   bits: 21/20
c ---[ 556]---> Adder-cost: 860   maxlim: 2031596   bits: 22/21
c ---[ 554]---> Adder-cost: 892   maxlim: 1409001   bits: 21/21
c ---[ 552]---> Adder-cost: 652   maxlim: 1441776   bits: 21/21
c ---[ 550]---> Adder-cost: 702   maxlim: 1703920   bits: 22/21
c ---[ 548]---> Adder-cost: 893   maxlim: 2228202   bits: 22/22
c ---[ 546]---> Adder-cost: 1006   maxlim: 2883559   bits: 22/22
c ---[ 544]---> Adder-cost: 133886   maxlim: 516959487   bits: 30/29
c ---[ 542]---> Adder-cost: 13882   maxlim: 43122275   bits: 26/26
c ---[ 540]---> Adder-cost: 45292   maxlim: 90176735   bits: 28/27
c ---[ 538]---> Adder-cost: 60472   maxlim: 112245487   bits: 28/27
c ---[ 536]---> Adder-cost: 54534   maxlim: 137460392   bits: 28/28
c ---[ 534]---> Adder-cost: 17012   maxlim: 40304183   bits: 26/26
c ---[ 532]---> Adder-cost: 5799   maxlim: 9207713   bits: 25/24
c ---[ 530]---> Adder-cost: 3107   maxlim: 3047374   bits: 23/22
c ---[ 528]---> Adder-cost: 3199   maxlim: 6291373   bits: 24/23
c ---[ 526]---> Adder-cost: 33808   maxlim: 51838357   bits: 27/26
c ---[ 524]---> Adder-cost: 7908   maxlim: 13041496   bits: 25/24
c ---[ 522]---> Adder-cost: 4977   maxlim: 4489151   bits: 24/23
c ---[ 520]---> Adder-cost: 11088   maxlim: 17497923   bits: 26/25
c ---[ 518]---> Adder-cost: 286   maxlim: 425978   bits: 20/19
c ---[ 516]---> Adder-cost: 2505   maxlim: 4718536   bits: 23/23
c ---[ 514]---> Adder-cost: 6709   maxlim: 6553504   bits: 24/23
c ---[ 512]---> Adder-cost: 4987   maxlim: 5636020   bits: 24/23
c ---[ 510]---> Adder-cost: 722   maxlim: 1048557   bits: 21/20
c ---[ 508]---> Adder-cost: 1008   maxlim: 1474533   bits: 21/21
c ---[ 506]---> Adder-cost: 946   maxlim: 1343465   bits: 21/21
c ---[ 504]---> Adder-cost: 1008   maxlim: 1507300   bits: 21/21
c ---[ 502]---> Adder-cost: 696   maxlim: 1015790   bits: 21/20
c ---[ 500]---> Adder-cost: 700   maxlim: 1015790   bits: 21/20
c ---[ 498]---> Adder-cost: 672   maxlim: 1638385   bits: 22/21
c ---[ 496]---> Adder-cost: 652   maxlim: 1507312   bits: 21/21
c ---[ 494]---> Adder-cost: 416   maxlim: 327668   bits: 19/19
c ---[ 492]---> Adder-cost: 376   maxlim: 491510   bits: 20/19
c ---[ 490]---> Adder-cost: 728   maxlim: 1146858   bits: 21/21
c ---[ 488]---> Adder-cost: 668   maxlim: 1048558   bits: 21/20
c ---[ 486]---> Adder-cost: 678   maxlim: 524269   bits: 20/19
c ---[ 484]---> Adder-cost: 946   maxlim: 1408999   bits: 21/21
c ---[ 482]---> Adder-cost: 564   maxlim: 393202   bits: 20/19
c ---[ 480]---> Adder-cost: 1004   maxlim: 3014630   bits: 22/22
c ---[ 478]---> Adder-cost: 950   maxlim: 2949096   bits: 22/22
c ---[ 476]---> Adder-cost: 924   maxlim: 1343465   bits: 21/21
c ---[ 474]---> Adder-cost: 412   maxlim: 589813   bits: 20/20
c ---[ 472]---> Adder-cost: 916   maxlim: 1474535   bits: 21/21
c ---[ 470]---> Adder-cost: 696   maxlim: 1081324   bits: 21/21
c ---[ 468]---> Adder-cost: 416   maxlim: 753652   bits: 20/20
c ---[ 466]---> Adder-cost: 414   maxlim: 622581   bits: 20/20
c ---[ 464]---> Adder-cost: 740   maxlim: 2162669   bits: 22/22
c ---[ 462]---> Adder-cost: 740   maxlim: 2228205   bits: 22/22
c ---[ 460]---> Adder-cost: 974   maxlim: 2949095   bits: 22/22
c ---[ 458]---> Adder-cost: 576   maxlim: 1703922   bits: 22/21
c ---[ 456]---> Adder-cost: 636   maxlim: 1048559   bits: 21/20
c ---[ 454]---> Adder-cost: 416   maxlim: 327668   bits: 19/19
c ---[ 452]---> Adder-cost: 638   maxlim: 1769456   bits: 22/21
c ---[ 450]---> Adder-cost: 638   maxlim: 1507313   bits: 22/21
c ---[ 448]---> Adder-cost: 768   maxlim: 2293739   bits: 22/22
c ---[ 446]---> Adder-cost: 706   maxlim: 2228205   bits: 22/22
c ---[ 444]---> Adder-cost: 740   maxlim: 2162669   bits: 22/22
c ---[ 442]---> Adder-cost: 916   maxlim: 1474535   bits: 21/21
c ---[ 440]---> Adder-cost: 412   maxlim: 720885   bits: 20/20
c ---[ 438]---> Adder-cost: 406   maxlim: 622578   bits: 20/20
c ---[ 436]---> Adder-cost: 972   maxlim: 3014631   bits: 22/22
c ---[ 434]---> Adder-cost: 696   maxlim: 1015790   bits: 21/20
c ---[ 432]---> Adder-cost: 1004   maxlim: 2883559   bits: 22/22
c ---[ 430]---> Adder-cost: 982   maxlim: 2818024   bits: 22/22
c ---[ 428]---> Adder-cost: 916   maxlim: 1474535   bits: 21/21
c ---[ 426]---> Adder-cost: 638   maxlim: 1015791   bits: 21/20
c ---[ 424]---> Adder-cost: 650   maxlim: 524269   bits: 20/19
c ---[ 422]---> Adder-cost: 436   maxlim: 655347   bits: 20/20
c ---[ 420]---> Adder-cost: 330   maxlim: 246008   bits: 19/18
c ---[ 418]---> Adder-cost: 948   maxlim: 2523110   bits: 22/22
c ---[ 416]---> Adder-cost: 438   maxlim: 819188   bits: 20/20
c ---[ 414]---> Adder-cost: 576   maxlim: 1376240   bits: 21/21
c ---[ 412]---> Adder-cost: 578   maxlim: 1277937   bits: 21/21
c ---[ 410]---> Adder-cost: 1322   maxlim: 3964889   bits: 23/22
c ---[ 408]---> Adder-cost: 286   maxlim: 327674   bits: 20/19
c ---[ 406]---> Adder-cost: 948   maxlim: 2457573   bits: 22/22
c ---[ 404]---> Adder-cost: 1318   maxlim: 4030425   bits: 23/22
c ---[ 402]---> Adder-cost: 948   maxlim: 2392038   bits: 22/22
c ---[ 400]---> Adder-cost: 969   maxlim: 2424805   bits: 22/22
c ---[ 398]---> Adder-cost: 1329   maxlim: 4161497   bits: 23/22
c ---[ 396]---> Adder-cost: 956   maxlim: 2785253   bits: 22/22
c ---[ 394]---> Adder-cost: 922   maxlim: 2785253   bits: 22/22
c ---[ 392]---> Adder-cost: 684   maxlim: 933868   bits: 21/20
c ---[ 390]---> Adder-cost: 789   maxlim: 2424809   bits: 22/22
c ---[ 388]---> Adder-cost: 1319   maxlim: 4292568   bits: 23/23
c ---[ 386]---> Adder-cost: 1066   maxlim: 3014628   bits: 22/22
c ---[ 384]---> Adder-cost: 822   maxlim: 2326505   bits: 22/22
c ---[ 382]---> Adder-cost: 598   maxlim: 999405   bits: 21/20
c ---[ 380]---> Adder-cost: 528   maxlim: 819184   bits: 20/20
c ---[ 378]---> Adder-cost: 1300   maxlim: 2162667   bits: 23/22
c ---[ 376]---> Adder-cost: 786   maxlim: 2064361   bits: 22/21
c ---[ 374]---> Adder-cost: 828   maxlim: 1277938   bits: 22/21
c ---[ 372]---> Adder-cost: 1310   maxlim: 2555882   bits: 23/22
c ---[ 370]---> Adder-cost: 1309   maxlim: 2424811   bits: 23/22
c ---[ 368]---> Adder-cost: 1301   maxlim: 2293739   bits: 23/22
c ---[ 366]---> Adder-cost: 1310   maxlim: 2555882   bits: 23/22
c ---[ 364]---> Adder-cost: 1304   maxlim: 2228204   bits: 23/22
c ---[ 362]---> Adder-cost: 1310   maxlim: 2424811   bits: 23/22
c ---[ 360]---> Adder-cost: 524   maxlim: 1376242   bits: 21/21
c ---[ 358]---> Adder-cost: 1301   maxlim: 2424811   bits: 23/22
c ---[ 356]---> Adder-cost: 784   maxlim: 1736684   bits: 22/21
c ---[ 354]---> Adder-cost: 1064   maxlim: 2752486   bits: 22/22
c ---[ 352]---> Adder-cost: 918   maxlim: 917488   bits: 21/20
c ---[ 350]---> Adder-cost: 788   maxlim: 753651   bits: 21/20
c ---[ 348]---> Adder-cost: 1284   maxlim: 2424811   bits: 23/22
c ---[ 346]---> Adder-cost: 1243   maxlim: 2424811   bits: 23/22
c ---[ 344]---> Adder-cost: 1295   maxlim: 2359276   bits: 23/22
c ---[ 342]---> Adder-cost: 1310   maxlim: 2424811   bits: 23/22
c ---[ 340]---> Adder-cost: 1076   maxlim: 2818023   bits: 23/22
c ---[ 338]---> Adder-cost: 1281   maxlim: 2424811   bits: 23/22
c ---[ 336]---> Adder-cost: 882   maxlim: 1966059   bits: 22/21
c ---[ 334]---> Adder-cost: 1098   maxlim: 2818021   bits: 22/22
c ---[ 332]---> Adder-cost: 918   maxlim: 917488   bits: 21/20
c ---[ 330]---> Adder-cost: 738   maxlim: 1114096   bits: 21/21
c ---[ 328]---> Adder-cost: 816   maxlim: 1245168   bits: 22/21
c ---[ 326]---> Adder-cost: 945   maxlim: 1572844   bits: 22/21
c ---[ 324]---> Adder-cost: 982   maxlim: 1507308   bits: 22/21
c ---[ 322]---> Adder-cost: 1247   maxlim: 2064360   bits: 22/21
c ---[ 320]---> Adder-cost: 1246   maxlim: 2260965   bits: 22/22
c ---[ 318]---> Adder-cost: 1282   maxlim: 2129895   bits: 22/22
c ---[ 316]---> Adder-cost: 612   maxlim: 524275   bits: 20/19
c ---[ 314]---> Adder-cost: 1259   maxlim: 2228197   bits: 23/22
c ---[ 312]---> Adder-cost: 1313   maxlim: 2195430   bits: 22/22
c ---[ 310]---> Adder-cost: 1064   maxlim: 1900525   bits: 22/21
c ---[ 308]---> Adder-cost: 836   maxlim: 720879   bits: 21/20
c ---[ 306]---> Adder-cost: 582   maxlim: 491508   bits: 20/19
c ---[ 304]---> Adder-cost: 790   maxlim: 1966060   bits: 22/21
c ---[ 302]---> Adder-cost: 1158   maxlim: 1867756   bits: 22/21
c ---[ 300]---> Adder-cost: 1258   maxlim: 2129895   bits: 23/22
c ---[ 298]---> Adder-cost: 1088   maxlim: 966634   bits: 21/20
c ---[ 296]---> Adder-cost: 888   maxlim: 1540078   bits: 22/21
c ---[ 294]---> Adder-cost: 562   maxlim: 1114102   bits: 21/21
c ---[ 292]---> Adder-cost: 408   maxlim: 344057   bits: 20/19
c ---[ 290]---> Adder-cost: 1028   maxlim: 1834990   bits: 22/21
c ---[ 288]---> Adder-cost: 1096   maxlim: 1802221   bits: 22/21
c ---[ 286]---> Adder-cost: 406   maxlim: 360440   bits: 20/19
c ---[ 284]---> Adder-cost: 324   maxlim: 327670   bits: 19/19
c ---[ 282]---> Adder-cost: 618   maxlim: 1146859   bits: 21/21
c ---[ 280]---> Adder-cost: 358   maxlim: 393204   bits: 19/19
c ---[ 278]---> Adder-cost: 896   maxlim: 1474540   bits: 22/21
c ---[ 276]---> Adder-cost: 914   maxlim: 1540078   bits: 22/21
c ---[ 274]---> Adder-cost: 669   maxlim: 1245170   bits: 21/21
c ---[ 272]---> Adder-cost: 1149   maxlim: 2883556   bits: 23/22
c ---[ 270]---> Adder-cost: 783   maxlim: 1769451   bits: 22/21
c ---[ 268]---> Adder-cost: 1180   maxlim: 2555877   bits: 22/22
c ---[ 266]---> Adder-cost: 1135   maxlim: 2621413   bits: 23/22
c ---[ 264]---> Adder-cost: 1184   maxlim: 2555878   bits: 23/22
c ---[ 262]---> Adder-cost: 1150   maxlim: 2621413   bits: 22/22
c ---[ 260]---> Adder-cost: 925   maxlim: 1900523   bits: 22/21
c ---[ 258]---> Adder-cost: 848   maxlim: 1638383   bits: 22/21
c ---[ 256]---> Adder-cost: 1166   maxlim: 2621413   bits: 22/22
c ---[ 254]---> Adder-cost: 768   maxlim: 2162668   bits: 22/22
c ---[ 252]---> Adder-cost: 1137   maxlim: 2686948   bits: 22/22
c ---[ 250]---> Adder-cost: 850   maxlim: 1703916   bits: 22/21
c ---[ 248]---> Adder-cost: 1147   maxlim: 2752483   bits: 22/22
c ---[ 246]---> Adder-cost: 1097   maxlim: 2490343   bits: 22/22
c ---[ 244]---> Adder-cost: 1140   maxlim: 2490343   bits: 23/22
c ---[ 242]---> Adder-cost: 1062   maxlim: 1245159   bits: 21/21
c ---[ 240]---> Adder-cost: 896   maxlim: 1703918   bits: 22/21
c ---[ 238]---> Adder-cost: 1180   maxlim: 2424806   bits: 22/22
c ---[ 236]---> Adder-cost: 879   maxlim: 1638381   bits: 22/21
c ---[ 234]---> Adder-cost: 860   maxlim: 1703918   bits: 22/21
c ---[ 232]---> Adder-cost: 1112   maxlim: 2490343   bits: 22/22
c ---[ 230]---> Adder-cost: 560   maxlim: 540661   bits: 20/20
c ---[ 228]---> Adder-cost: 598   maxlim: 671731   bits: 21/20
c ---[ 226]---> Adder-cost: 710   maxlim: 1638383   bits: 22/21
c ---[ 224]---> Adder-cost: 724   maxlim: 1507312   bits: 22/21
c ---[ 222]---> Adder-cost: 1192   maxlim: 2621413   bits: 22/22
c ---[ 220]---> Adder-cost: 1026   maxlim: 1245159   bits: 21/21
c ---[ 218]---> Adder-cost: 1168   maxlim: 2555878   bits: 22/22
c ---[ 216]---> Adder-cost: 1092   maxlim: 2424808   bits: 22/22
c ---[ 214]---> Adder-cost: 918   maxlim: 1097708   bits: 21/21
c ---[ 212]---> Adder-cost: 1360   maxlim: 2949084   bits: 22/22
c ---[ 210]---> Adder-cost: 984   maxlim: 2129896   bits: 22/22
c ---[ 208]---> Adder-cost: 984   maxlim: 2064360   bits: 22/21
c ---[ 206]---> Adder-cost: 1348   maxlim: 2981854   bits: 23/22
c ---[ 204]---> Adder-cost: 963   maxlim: 2162663   bits: 22/22
c ---[ 202]---> Adder-cost: 924   maxlim: 2162664   bits: 22/22
c ---[ 200]---> Adder-cost: 960   maxlim: 2260968   bits: 22/22
c ---[ 198]---> Adder-cost: 1285   maxlim: 3243997   bits: 23/22
c ---[ 196]---> Adder-cost: 969   maxlim: 2129896   bits: 22/22
c ---[ 194]---> Adder-cost: 960   maxlim: 2326504   bits: 22/22
c ---[ 192]---> Adder-cost: 1306   maxlim: 3178461   bits: 23/22
c ---[ 190]---> Adder-cost: 1016   maxlim: 2129896   bits: 22/22
c ---[ 188]---> Adder-cost: 1347   maxlim: 3047390   bits: 23/22
c ---[ 186]---> Adder-cost: 1375   maxlim: 3047388   bits: 23/22
c ---[ 184]---> Adder-cost: 1334   maxlim: 2981854   bits: 23/22
c ---[ 182]---> Adder-cost: 708   maxlim: 835565   bits: 21/20
c ---[ 180]---> Adder-cost: 668   maxlim: 786414   bits: 21/20
c ---[ 178]---> Adder-cost: 1171   maxlim: 1736684   bits: 22/21
c ---[ 176]---> Adder-cost: 1537   maxlim: 2457575   bits: 23/22
c ---[ 174]---> Adder-cost: 1179   maxlim: 1834988   bits: 22/21
c ---[ 172]---> Adder-cost: 1497   maxlim: 2490342   bits: 23/22
c ---[ 170]---> Adder-cost: 1165   maxlim: 1834988   bits: 22/21
c ---[ 168]---> Adder-cost: 1549   maxlim: 2424808   bits: 23/22
c ---[ 166]---> Adder-cost: 1066   maxlim: 3080164   bits: 22/22
c ---[ 164]---> Adder-cost: 633   maxlim: 688114   bits: 21/20
c ---[ 162]---> Adder-cost: 786   maxlim: 1376236   bits: 21/21
c ---[ 160]---> Adder-cost: 646   maxlim: 1343471   bits: 21/21
c ---[ 158]---> Adder-cost: 1065   maxlim: 2359266   bits: 22/22
c ---[ 156]---> Adder-cost: 1095   maxlim: 2260963   bits: 22/22
c ---[ 154]---> Adder-cost: 1058   maxlim: 2490338   bits: 22/22
c ---[ 152]---> Adder-cost: 1000   maxlim: 1343469   bits: 22/21
c ---[ 150]---> Adder-cost: 1032   maxlim: 1441771   bits: 22/21
c ---[ 148]---> Adder-cost: 936   maxlim: 1245167   bits: 22/21
c ---[ 146]---> Adder-cost: 1287   maxlim: 1867751   bits: 22/21
c ---[ 144]---> Adder-cost: 840   maxlim: 1146861   bits: 22/21
c ---[ 142]---> Adder-cost: 1315   maxlim: 1933285   bits: 22/21
c ---[ 140]---> Adder-cost: 1311   maxlim: 1900518   bits: 22/21
c ---[ 138]---> Adder-cost: 1323   maxlim: 1900518   bits: 22/21
c ---[ 136]---> Adder-cost: 1016   maxlim: 1703919   bits: 22/21
c ---[ 134]---> Adder-cost: 882   maxlim: 1146865   bits: 22/21
c ---[ 132]---> Adder-cost: 1325   maxlim: 1867751   bits: 22/21
c ---[ 130]---> Adder-cost: 1070   maxlim: 1507310   bits: 22/21
c ---[ 128]---> Adder-cost: 1042   maxlim: 770285   bits: 21/20
c ---[ 126]---> Adder-cost: 1206   maxlim: 1703914   bits: 22/21
c ---[ 124]---> Adder-cost: 958   maxlim: 1572847   bits: 22/21
c ---[ 122]---> Adder-cost: 1078   maxlim: 1638381   bits: 22/21
c ---[ 120]---> Adder-cost: 948   maxlim: 688369   bits: 21/20
c ---[ 118]---> Adder-cost: 1168   maxlim: 1638379   bits: 22/21
c ---[ 116]---> Adder-cost: 1049   maxlim: 1540079   bits: 22/21
c ---[ 114]---> Adder-cost: 330   maxlim: 622585   bits: 21/20
c ---[ 112]---> Adder-cost: 1029   maxlim: 1638377   bits: 22/21
c ---[ 110]---> Adder-cost: 1413   maxlim: 2392031   bits: 22/22
c ---[ 108]---> Adder-cost: 1000   maxlim: 1540076   bits: 22/21
c ---[ 106]---> Adder-cost: 950   maxlim: 1540076   bits: 22/21
c ---[ 104]---> Adder-cost: 1048   maxlim: 1114092   bits: 22/21
c ---[ 102]---> Adder-cost: 1039   maxlim: 1048557   bits: 21/20
c ---[ 100]---> Adder-cost: 730   maxlim: 720887   bits: 21/20
c ---[  98]---> Adder-cost: 1225   maxlim: 1212396   bits: 22/21
c ---[  96]---> Adder-cost: 730   maxlim: 720887   bits: 21/20
c ---[  94]---> Adder-cost: 748   maxlim: 655351   bits: 21/20
c ---[  92]---> Adder-cost: 541   maxlim: 458745   bits: 20/19
c ---[  90]---> Adder-cost: 977   maxlim: 1015790   bits: 21/20
c ---[  88]---> Adder-cost: 768   maxlim: 688118   bits: 21/20
c ---[  86]---> Adder-cost: 1241   maxlim: 1212396   bits: 22/21
c ---[  84]---> Adder-cost: 479   maxlim: 425978   bits: 20/19
c ---[  82]---> Sorter-cost:  762     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  80]---> Adder-cost: 456   maxlim: 819189   bits: 20/20
c ---[  78]---> Adder-cost: 926   maxlim: 2490342   bits: 22/22
c ---[  76]---> Adder-cost: 967   maxlim: 2457573   bits: 22/22
c ---[  74]---> Adder-cost: 744   maxlim: 1834988   bits: 22/21
c ---[  72]---> Adder-cost: 936   maxlim: 2424807   bits: 22/22
c ---[  70]---> Adder-cost: 1317   maxlim: 3506140   bits: 23/22
c ---[  68]---> Adder-cost: 386   maxlim: 917494   bits: 21/20
c ---[  66]---> Adder-cost: 777   maxlim: 2195433   bits: 22/22
c ---[  64]---> Sorter-cost: 1593     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  62]---> Adder-cost: 910   maxlim: 1376240   bits: 22/21
c ---[  60]---> Adder-cost: 1428   maxlim: 2523112   bits: 23/22
c ---[  58]---> Adder-cost: 1409   maxlim: 2523112   bits: 23/22
c ---[  56]---> Adder-cost: 880   maxlim: 1540081   bits: 22/21
c ---[  54]---> Adder-cost: 767   maxlim: 1638377   bits: 21/21
c ---[  52]---> Adder-cost: 1030   maxlim: 2392035   bits: 22/22
c ---[  50]---> Adder-cost: 897   maxlim: 1933287   bits: 22/21
c ---[  48]---> Adder-cost: 322   maxlim: 688119   bits: 20/20
c ---[  46]---> Adder-cost: 972   maxlim: 1376237   bits: 22/21
c ---[  44]---> Adder-cost: 1262   maxlim: 2031590   bits: 22/21
c ---[  42]---> Adder-cost: 885   maxlim: 1277936   bits: 22/21
c ---[  40]---> Adder-cost: 966   maxlim: 1343470   bits: 22/21
c ---[  38]---> Adder-cost: 906   maxlim: 1343471   bits: 22/21
c ---[  36]---> Adder-cost: 1301   maxlim: 2031590   bits: 22/21
c ---[  34]---> Adder-cost: 965   maxlim: 1409004   bits: 22/21
c ---[  32]---> Adder-cost: 1061   maxlim: 1769451   bits: 22/21
c ---[  30]---> Adder-cost: 883   maxlim: 1179634   bits: 22/21
c ---[  28]---> Adder-cost: 367   maxlim: 229370   bits: 19/18
c ---[  26]---> Adder-cost: 735   maxlim: 917491   bits: 21/20
c ---[  24]---> Adder-cost: 816   maxlim: 1146867   bits: 22/21
c ---[  22]---> Adder-cost: 460   maxlim: 655351   bits: 21/20
c ---[  20]---> Adder-cost: 866   maxlim: 1245168   bits: 22/21
c ---[  18]---> Adder-cost: 1274   maxlim: 2097125   bits: 22/21
c ---[  16]---> Adder-cost: 1203   maxlim: 1834986   bits: 22/21
c ---[  14]---> Adder-cost: 812   maxlim: 1179633   bits: 22/21
c ---[  12]---> Adder-cost: 807   maxlim: 1179634   bits: 22/21
c ---[  10]---> Adder-cost: 968   maxlim: 1409005   bits: 22/21
c ---[   8]---> Adder-cost: 888   maxlim: 1277936   bits: 22/21
c ---[   6]---> Adder-cost: 433   maxlim: 458744   bits: 20/19
c ---[   4]---> Adder-cost: 768   maxlim: 1146863   bits: 21/21
c ---[   2]---> Adder-cost: 812   maxlim: 1245167   bits: 22/21
c ---[   0]---> Adder-cost: 934   maxlim: 1507309   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 9053897 32289967 | 3017965       0        0     nan |  0.000 % |
c |       100 | 9053897 32289967 | 3319761     100      306     3.1 |  2.734 % |
c |       250 | 9053881 32289915 | 3651737     248      812     3.3 |  2.734 % |
c |       475 | 9053875 32289897 | 4016911     472     1559     3.3 |  2.734 % |
c |       812 | 9053859 32289845 | 4418602     807     2796     3.5 |  2.734 % |
c |      1318 | 9053843 32289793 | 4860462    1311     4505     3.4 |  2.734 % |
c |      2077 | 9053811 32289689 | 5346509    2066     7129     3.5 |  2.734 % |
c |      3216 | 9053787 32289611 | 5881160    3202    11071     3.5 |  2.735 % |
c |      4924 | 9053735 32289441 | 6469276    4903    17494     3.6 |  2.735 % |
c |      7486 | 9053654 32289178 | 7116203    7455    26970     3.6 |  2.736 % |
c |     11330 | 9053544 32288822 | 7827823   11285    41338     3.7 |  2.737 % |
c |     17096 | 9051397 32281251 | 8610606   16772    61287     3.7 |  2.762 % |

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/15252/stat): 15252 (minisat+_script) R 15251 15252 21452 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1854979659 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/15252/statm): 174 3 169 147 0 27 0
[pid=15252] vsize: 696
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libtermcap.so.2
open syscall for file tls/i686/libtermcap.so.2
open syscall for file tls/mmx/libtermcap.so.2
open syscall for file tls/libtermcap.so.2
open syscall for file i686/mmx/libtermcap.so.2
open syscall for file i686/libtermcap.so.2
open syscall for file mmx/libtermcap.so.2
open syscall for file libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/libtermcap.so.2
open syscall for file /etc/ld.so.cache
open syscall for file /lib/libtermcap.so.2
open syscall for file tls/i686/mmx/libdl.so.2
open syscall for file tls/i686/libdl.so.2
open syscall for file tls/mmx/libdl.so.2
open syscall for file tls/libdl.so.2
open syscall for file i686/mmx/libdl.so.2
open syscall for file i686/libdl.so.2
open syscall for file mmx/libdl.so.2
open syscall for file libdl.so.2
open syscall for file /oldhome/oroussel/lib/libdl.so.2
open syscall for file /lib/libdl.so.2
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /lib/tls/libc.so.6
open syscall for file /dev/tty
open syscall for file /etc/mtab
open syscall for file /proc/meminfo
open syscall for file /oldhome/oroussel/solvers/minisat+_script
New process pid=15253
New process pid=15254
New process pid=15255
execve syscall for /bin/sed executable
One traced child (pid=15254) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=15255) exited with status: 0
One traced child (pid=15253) exited with status: 0
New process pid=15256
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-d6cube.opb

[startup+10.0034 s]
Raw data (loadavg): 0.94 0.96 0.91 1/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) T 15252 15252 21452 0 -1 0 28822 0 0 0 813 107 0 0 20 0 1 0 1854979664 71692288 9277 4294967295 134512640 135094434 3221224432 3221222652 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/15256/statm): 17503 9277 145 145 0 17358 0
[pid=15256] vsize: 70012
Current children cumulated CPU time (s) 9.2
Current children cumulated vsize (Kb) 72136

[startup+20.0041 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 1775 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134580034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0
[pid=15256] vsize: 86204
Current children cumulated CPU time (s) 18.99
Current children cumulated vsize (Kb) 88328

[startup+30.0048 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 2775 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134580024 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0
[pid=15256] vsize: 86204
Current children cumulated CPU time (s) 28.99
Current children cumulated vsize (Kb) 88328

[startup+40.0055 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 3776 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134579970 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0
[pid=15256] vsize: 86204
Current children cumulated CPU time (s) 39
Current children cumulated vsize (Kb) 88328

[startup+50.0062 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 4776 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134581225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0
[pid=15256] vsize: 86204
Current children cumulated CPU time (s) 49
Current children cumulated vsize (Kb) 88328

[startup+60.0069 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 5776 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134579970 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0
[pid=15256] vsize: 86204
Current children cumulated CPU time (s) 59
Current children cumulated vsize (Kb) 88328

[startup+70.0076 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 6776 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134581225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0
[pid=15256] vsize: 86204
Current children cumulated CPU time (s) 69
Current children cumulated vsize (Kb) 88328

[startup+80.0083 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 7777 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134581225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0
[pid=15256] vsize: 86204
Current children cumulated CPU time (s) 79.01
Current children cumulated vsize (Kb) 88328

[startup+90.009 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 8777 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134581225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0
[pid=15256] vsize: 86204
Current children cumulated CPU time (s) 89.01
Current children cumulated vsize (Kb) 88328

[startup+100.009 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 9777 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134579997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0
[pid=15256] vsize: 86204
Current children cumulated CPU time (s) 99.01
Current children cumulated vsize (Kb) 88328

[startup+110.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 10777 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134580048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0
[pid=15256] vsize: 86204
Current children cumulated CPU time (s) 109.01
Current children cumulated vsize (Kb) 88328

[startup+120.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 11777 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134579970 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0
[pid=15256] vsize: 86204
Current children cumulated CPU time (s) 119.01
Current children cumulated vsize (Kb) 88328

[startup+130.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 12777 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134579970 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0
[pid=15256] vsize: 86204
Current children cumulated CPU time (s) 129.01
Current children cumulated vsize (Kb) 88328

[startup+140.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 13777 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134581225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0
[pid=15256] vsize: 86204
Current children cumulated CPU time (s) 139.01
Current children cumulated vsize (Kb) 88328

[startup+150.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 14778 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134581225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0
[pid=15256] vsize: 86204
Current children cumulated CPU time (s) 149.02
Current children cumulated vsize (Kb) 88328

[startup+160.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 15778 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134579970 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0
[pid=15256] vsize: 86204
Current children cumulated CPU time (s) 159.02
Current children cumulated vsize (Kb) 88328

[startup+170.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 16778 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134581225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0
[pid=15256] vsize: 86204
Current children cumulated CPU time (s) 169.02
Current children cumulated vsize (Kb) 88328

[startup+180.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 17778 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134579968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0
[pid=15256] vsize: 86204
Current children cumulated CPU time (s) 179.02
Current children cumulated vsize (Kb) 88328

[startup+190.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 18779 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134579970 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0
[pid=15256] vsize: 86204
Current children cumulated CPU time (s) 189.03
Current children cumulated vsize (Kb) 88328

[startup+200.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 19779 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134580034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0
[pid=15256] vsize: 86204
Current children cumulated CPU time (s) 199.03
Current children cumulated vsize (Kb) 88328

[startup+210.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 20779 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134580075 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0
[pid=15256] vsize: 86204
Current children cumulated CPU time (s) 209.03
Current children cumulated vsize (Kb) 88328

[startup+220.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 21779 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134580048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0
[pid=15256] vsize: 86204
Current children cumulated CPU time (s) 219.03
Current children cumulated vsize (Kb) 88328

[startup+230.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 22779 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134581212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0
[pid=15256] vsize: 86204
Current children cumulated CPU time (s) 229.03
Current children cumulated vsize (Kb) 88328

[startup+240.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 23780 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134581225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0
[pid=15256] vsize: 86204
Current children cumulated CPU time (s) 239.04
Current children cumulated vsize (Kb) 88328

[startup+250.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 24780 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134579970 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0
[pid=15256] vsize: 86204
Current children cumulated CPU time (s) 249.04
Current children cumulated vsize (Kb) 88328

[startup+260.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 25780 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134581225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0
[pid=15256] vsize: 86204
Current children cumulated CPU time (s) 259.04
Current children cumulated vsize (Kb) 88328

[startup+270.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 26780 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134581225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0
[pid=15256] vsize: 86204
Current children cumulated CPU time (s) 269.04
Current children cumulated vsize (Kb) 88328

[startup+280.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 27781 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134581225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0
[pid=15256] vsize: 86204
Current children cumulated CPU time (s) 279.05
Current children cumulated vsize (Kb) 88328

[startup+290.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 28781 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134580017 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0
[pid=15256] vsize: 86204
Current children cumulated CPU time (s) 289.05
Current children cumulated vsize (Kb) 88328

[startup+300.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 29781 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134580081 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0
[pid=15256] vsize: 86204
Current children cumulated CPU time (s) 299.05
Current children cumulated vsize (Kb) 88328

[startup+310.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 30781 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134581225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0
[pid=15256] vsize: 86204
Current children cumulated CPU time (s) 309.05
Current children cumulated vsize (Kb) 88328

[startup+320.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 31782 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134581225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0
[pid=15256] vsize: 86204
Current children cumulated CPU time (s) 319.06
Current children cumulated vsize (Kb) 88328

[startup+330.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 32782 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134581225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0
[pid=15256] vsize: 86204
Current children cumulated CPU time (s) 329.06
Current children cumulated vsize (Kb) 88328

[startup+340.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 33782 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134580034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0
[pid=15256] vsize: 86204
Current children cumulated CPU time (s) 339.06
Current children cumulated vsize (Kb) 88328

[startup+350.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 34782 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134580048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0
[pid=15256] vsize: 86204
Current children cumulated CPU time (s) 349.06
Current children cumulated vsize (Kb) 88328

[startup+360.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 35783 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134580024 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0
[pid=15256] vsize: 86204
Current children cumulated CPU time (s) 359.07
Current children cumulated vsize (Kb) 88328

[startup+370.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 36783 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134581225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0
[pid=15256] vsize: 86204
Current children cumulated CPU time (s) 369.07
Current children cumulated vsize (Kb) 88328

[startup+380.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 37783 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134581225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0
[pid=15256] vsize: 86204
Current children cumulated CPU time (s) 379.07
Current children cumulated vsize (Kb) 88328

[startup+390.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 38783 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134581225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0
[pid=15256] vsize: 86204
Current children cumulated CPU time (s) 389.07
Current children cumulated vsize (Kb) 88328

[startup+400.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 39783 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134579970 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0
[pid=15256] vsize: 86204
Current children cumulated CPU time (s) 399.07
Current children cumulated vsize (Kb) 88328

[startup+410.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 40784 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134581225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0
[pid=15256] vsize: 86204
Current children cumulated CPU time (s) 409.08
Current children cumulated vsize (Kb) 88328

[startup+420.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 41784 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134580028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0
[pid=15256] vsize: 86204
Current children cumulated CPU time (s) 419.08
Current children cumulated vsize (Kb) 88328

[startup+430.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 42784 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134579970 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0
[pid=15256] vsize: 86204
Current children cumulated CPU time (s) 429.08
Current children cumulated vsize (Kb) 88328

[startup+440.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 39241 0 0 0 43771 138 0 0 25 0 1 0 1854979664 110428160 18608 4294967295 134512640 135094434 3221224432 3203806560 134596860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 26960 18608 145 145 0 26815 0
[pid=15256] vsize: 107840
Current children cumulated CPU time (s) 439.09
Current children cumulated vsize (Kb) 109964

[startup+450.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 48908 0 0 0 44726 164 0 0 25 0 1 0 1854979664 134586368 23877 4294967295 134512640 135094434 3221224432 3221221808 134601016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 32858 23877 145 145 0 32713 0
[pid=15256] vsize: 131432
Current children cumulated CPU time (s) 448.9
Current children cumulated vsize (Kb) 133556

[startup+460.034 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) T 15252 15252 21452 0 -1 0 67335 0 0 0 45649 216 0 0 23 0 1 0 1854979664 186015744 35726 4294967295 134512640 135094434 3221224432 3221221212 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/15256/statm): 45414 35726 145 145 0 45269 0
[pid=15256] vsize: 181656
Current children cumulated CPU time (s) 458.65
Current children cumulated vsize (Kb) 183780

[startup+470.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 93124 0 0 0 46521 292 0 0 25 0 1 0 1854979664 263110656 53721 4294967295 134512640 135094434 3221224432 3210860288 134597014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15256/statm): 64236 53721 145 145 0 64091 0
[pid=15256] vsize: 256944
Current children cumulated CPU time (s) 468.13
Current children cumulated vsize (Kb) 259068

[startup+480.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 97671 0 0 0 47504 304 0 0 25 0 1 0 1854979664 263004160 53695 4294967295 134512640 135094434 3221224432 3215684656 134597418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15256/statm): 64210 53695 145 145 0 64065 0
[pid=15256] vsize: 256840
Current children cumulated CPU time (s) 478.08
Current children cumulated vsize (Kb) 258964

[startup+490.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 101823 0 0 0 48487 316 0 0 25 0 1 0 1854979664 261255168 53171 4294967295 134512640 135094434 3221224432 3221221984 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15256/statm): 63783 53171 145 145 0 63638 0
[pid=15256] vsize: 255132
Current children cumulated CPU time (s) 488.03
Current children cumulated vsize (Kb) 257256

[startup+500.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 105216 0 0 0 49475 324 0 0 25 0 1 0 1854979664 260730880 53089 4294967295 134512640 135094434 3221224432 3221222576 134677091 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15256/statm): 63655 53089 145 145 0 63510 0
[pid=15256] vsize: 254620
Current children cumulated CPU time (s) 497.99
Current children cumulated vsize (Kb) 256744

[startup+510.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 109594 0 0 0 50457 338 0 0 25 0 1 0 1854979664 263352320 53654 4294967295 134512640 135094434 3221224432 3221222160 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15256/statm): 64295 53654 145 145 0 64150 0
[pid=15256] vsize: 257180
Current children cumulated CPU time (s) 507.95
Current children cumulated vsize (Kb) 259304

[startup+520.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 112056 0 0 0 51448 345 0 0 25 0 1 0 1854979664 260206592 53012 4294967295 134512640 135094434 3221224432 3221223120 134596445 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15256/statm): 63527 53012 145 145 0 63382 0
[pid=15256] vsize: 254108
Current children cumulated CPU time (s) 517.93
Current children cumulated vsize (Kb) 256232

[startup+530.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 115522 0 0 0 52435 355 0 0 25 0 1 0 1854979664 260206592 53012 4294967295 134512640 135094434 3221224432 3221223120 134596398 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15256/statm): 63527 53012 145 145 0 63382 0
[pid=15256] vsize: 254108
Current children cumulated CPU time (s) 527.9
Current children cumulated vsize (Kb) 256232

[startup+540.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 116323 0 0 0 53432 356 0 0 25 0 1 0 1854979664 260206592 53012 4294967295 134512640 135094434 3221224432 3221222708 134520000 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15256/statm): 63527 53012 145 145 0 63382 0
[pid=15256] vsize: 254108
Current children cumulated CPU time (s) 537.88
Current children cumulated vsize (Kb) 256232

[startup+550.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 116323 0 0 0 54432 356 0 0 25 0 1 0 1854979664 260206592 53012 4294967295 134512640 135094434 3221224432 3221220448 134680380 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15256/statm): 63527 53012 145 145 0 63382 0
[pid=15256] vsize: 254108
Current children cumulated CPU time (s) 547.88
Current children cumulated vsize (Kb) 256232

[startup+560.044 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) T 15252 15252 21452 0 -1 0 133266 0 0 0 55302 423 0 0 21 0 1 0 1854979664 307818496 67346 4294967295 134512640 135094434 3221224432 3221212764 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/15256/statm): 75151 67346 145 145 0 75006 0
[pid=15256] vsize: 300604
Current children cumulated CPU time (s) 557.25
Current children cumulated vsize (Kb) 302728

[startup+570.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 161687 0 0 0 56037 548 0 0 22 0 1 0 1854979664 437772288 95767 4294967295 134512640 135094434 3221224432 3221213840 134553146 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15256/statm): 106878 95767 145 145 0 106733 0
[pid=15256] vsize: 427512
Current children cumulated CPU time (s) 565.85
Current children cumulated vsize (Kb) 429636

[startup+580.045 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) T 15252 15252 21452 0 -1 0 190315 0 0 0 56780 668 0 0 22 0 1 0 1854979664 550719488 124395 4294967295 134512640 135094434 3221224432 3221216540 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/15256/statm): 134453 124395 145 145 0 134308 0
[pid=15256] vsize: 537812
Current children cumulated CPU time (s) 574.48
Current children cumulated vsize (Kb) 539936

[startup+590.046 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) T 15252 15252 21452 0 -1 0 219282 0 0 0 57514 792 0 0 21 0 1 0 1854979664 704372736 153362 4294967295 134512640 135094434 3221224432 3221216444 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/15256/statm): 171966 153362 145 145 0 171821 0
[pid=15256] vsize: 687864
Current children cumulated CPU time (s) 583.06
Current children cumulated vsize (Kb) 689988

[startup+600.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 241571 0 0 0 58311 890 0 0 25 0 1 0 1854979664 819052544 175651 4294967295 134512640 135094434 3221224432 3221223248 134558992 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 199964 175651 145 145 0 199819 0
[pid=15256] vsize: 799856
Current children cumulated CPU time (s) 592.01
Current children cumulated vsize (Kb) 801980

[startup+610.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 241581 0 0 0 59311 890 0 0 25 0 1 0 1854979664 819060736 175661 4294967295 134512640 135094434 3221224432 3221223136 134559005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15256/statm): 199966 175661 145 145 0 199821 0
[pid=15256] vsize: 799864
Current children cumulated CPU time (s) 602.01
Current children cumulated vsize (Kb) 801988

[startup+620.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 241583 0 0 0 60311 891 0 0 25 0 1 0 1854979664 819068928 175663 4294967295 134512640 135094434 3221224432 3221223100 134553438 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 199968 175663 145 145 0 199823 0
[pid=15256] vsize: 799872
Current children cumulated CPU time (s) 612.02
Current children cumulated vsize (Kb) 801996

[startup+630.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 241588 0 0 0 61311 891 0 0 25 0 1 0 1854979664 819093504 175668 4294967295 134512640 135094434 3221224432 3221223116 134553432 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 199974 175668 145 145 0 199829 0
[pid=15256] vsize: 799896
Current children cumulated CPU time (s) 622.02
Current children cumulated vsize (Kb) 802020

[startup+640.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 241599 0 0 0 62311 891 0 0 25 0 1 0 1854979664 819138560 175679 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 199985 175679 145 145 0 199840 0
[pid=15256] vsize: 799940
Current children cumulated CPU time (s) 632.02
Current children cumulated vsize (Kb) 802064

[startup+650.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 241705 0 0 0 63309 891 0 0 25 0 1 0 1854979664 819568640 175785 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 200090 175785 145 145 0 199945 0
[pid=15256] vsize: 800360
Current children cumulated CPU time (s) 642
Current children cumulated vsize (Kb) 802484

[startup+660.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 241783 0 0 0 64308 892 0 0 25 0 1 0 1854979664 819888128 175863 4294967295 134512640 135094434 3221224432 3221223120 134558992 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 200168 175863 145 145 0 200023 0
[pid=15256] vsize: 800672
Current children cumulated CPU time (s) 652
Current children cumulated vsize (Kb) 802796

[startup+670.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 241852 0 0 0 65308 892 0 0 25 0 1 0 1854979664 820183040 175932 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 200240 175932 145 145 0 200095 0
[pid=15256] vsize: 800960
Current children cumulated CPU time (s) 662
Current children cumulated vsize (Kb) 803084

[startup+680.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 242033 0 0 0 66305 893 0 0 25 0 1 0 1854979664 820920320 176113 4294967295 134512640 135094434 3221224432 3221223044 134563110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 200420 176113 145 145 0 200275 0
[pid=15256] vsize: 801680
Current children cumulated CPU time (s) 671.98
Current children cumulated vsize (Kb) 803804

[startup+690.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 242060 0 0 0 67305 893 0 0 25 0 1 0 1854979664 821039104 176140 4294967295 134512640 135094434 3221224432 3221223092 134553494 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 200449 176140 145 145 0 200304 0
[pid=15256] vsize: 801796
Current children cumulated CPU time (s) 681.98
Current children cumulated vsize (Kb) 803920

[startup+700.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 242109 0 0 0 68304 894 0 0 25 0 1 0 1854979664 821235712 176189 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 200497 176189 145 145 0 200352 0
[pid=15256] vsize: 801988
Current children cumulated CPU time (s) 691.98
Current children cumulated vsize (Kb) 804112

[startup+710.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 242216 0 0 0 69302 895 0 0 25 0 1 0 1854979664 821669888 176296 4294967295 134512640 135094434 3221224432 3221223092 134553533 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 200603 176296 145 145 0 200458 0
[pid=15256] vsize: 802412
Current children cumulated CPU time (s) 701.97
Current children cumulated vsize (Kb) 804536

[startup+720.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 242322 0 0 0 70301 895 0 0 25 0 1 0 1854979664 822104064 176402 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 200709 176402 145 145 0 200564 0
[pid=15256] vsize: 802836
Current children cumulated CPU time (s) 711.96
Current children cumulated vsize (Kb) 804960

[startup+730.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 242431 0 0 0 71299 896 0 0 25 0 1 0 1854979664 822546432 176511 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 200817 176511 145 145 0 200672 0
[pid=15256] vsize: 803268
Current children cumulated CPU time (s) 721.95
Current children cumulated vsize (Kb) 805392

[startup+740.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 242503 0 0 0 72298 896 0 0 25 0 1 0 1854979664 822870016 176583 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 200896 176583 145 145 0 200751 0
[pid=15256] vsize: 803584
Current children cumulated CPU time (s) 731.94
Current children cumulated vsize (Kb) 805708

[startup+750.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 242628 0 0 0 73296 897 0 0 25 0 1 0 1854979664 823377920 176708 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 201020 176708 145 145 0 200875 0
[pid=15256] vsize: 804080
Current children cumulated CPU time (s) 741.93
Current children cumulated vsize (Kb) 806204

[startup+760.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 242726 0 0 0 74294 897 0 0 25 0 1 0 1854979664 823779328 176806 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 201118 176806 145 145 0 200973 0
[pid=15256] vsize: 804472
Current children cumulated CPU time (s) 751.91
Current children cumulated vsize (Kb) 806596

[startup+770.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 242861 0 0 0 75292 898 0 0 25 0 1 0 1854979664 824328192 176941 4294967295 134512640 135094434 3221224432 3221223044 134563069 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 201252 176941 145 145 0 201107 0
[pid=15256] vsize: 805008
Current children cumulated CPU time (s) 761.9
Current children cumulated vsize (Kb) 807132

[startup+780.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 242979 0 0 0 76290 900 0 0 25 0 1 0 1854979664 824803328 177059 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 201368 177059 145 145 0 201223 0
[pid=15256] vsize: 805472
Current children cumulated CPU time (s) 771.9
Current children cumulated vsize (Kb) 807596

[startup+790.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243109 0 0 0 77288 901 0 0 25 0 1 0 1854979664 825335808 177189 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 201498 177189 145 145 0 201353 0
[pid=15256] vsize: 805992
Current children cumulated CPU time (s) 781.89
Current children cumulated vsize (Kb) 808116

[startup+800.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243180 0 0 0 78287 902 0 0 25 0 1 0 1854979664 825622528 177260 4294967295 134512640 135094434 3221224432 3221223072 134562108 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 201568 177260 145 145 0 201423 0
[pid=15256] vsize: 806272
Current children cumulated CPU time (s) 791.89
Current children cumulated vsize (Kb) 808396

[startup+810.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243345 0 0 0 79285 903 0 0 25 0 1 0 1854979664 826298368 177425 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 201733 177425 145 145 0 201588 0
[pid=15256] vsize: 806932
Current children cumulated CPU time (s) 801.88
Current children cumulated vsize (Kb) 809056

[startup+820.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243366 0 0 0 80285 903 0 0 25 0 1 0 1854979664 826380288 177446 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 201753 177446 145 145 0 201608 0
[pid=15256] vsize: 807012
Current children cumulated CPU time (s) 811.88
Current children cumulated vsize (Kb) 809136

[startup+830.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243400 0 0 0 81284 903 0 0 25 0 1 0 1854979664 826519552 177480 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 201787 177480 145 145 0 201642 0
[pid=15256] vsize: 807148
Current children cumulated CPU time (s) 821.87
Current children cumulated vsize (Kb) 809272

[startup+840.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243400 0 0 0 82285 903 0 0 25 0 1 0 1854979664 826519552 177480 4294967295 134512640 135094434 3221224432 3221223116 134553526 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 201787 177480 145 145 0 201642 0
[pid=15256] vsize: 807148
Current children cumulated CPU time (s) 831.88
Current children cumulated vsize (Kb) 809272

[startup+850.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243414 0 0 0 83284 903 0 0 25 0 1 0 1854979664 826576896 177494 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 201801 177494 145 145 0 201656 0
[pid=15256] vsize: 807204
Current children cumulated CPU time (s) 841.87
Current children cumulated vsize (Kb) 809328

[startup+860.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243434 0 0 0 84284 903 0 0 25 0 1 0 1854979664 826658816 177514 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 201821 177514 145 145 0 201676 0
[pid=15256] vsize: 807284
Current children cumulated CPU time (s) 851.87
Current children cumulated vsize (Kb) 809408

[startup+870.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243450 0 0 0 85284 903 0 0 25 0 1 0 1854979664 826724352 177530 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 201837 177530 145 145 0 201692 0
[pid=15256] vsize: 807348
Current children cumulated CPU time (s) 861.87
Current children cumulated vsize (Kb) 809472

[startup+880.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243463 0 0 0 86284 904 0 0 25 0 1 0 1854979664 826777600 177543 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 201850 177543 145 145 0 201705 0
[pid=15256] vsize: 807400
Current children cumulated CPU time (s) 871.88
Current children cumulated vsize (Kb) 809524

[startup+890.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243520 0 0 0 87283 904 0 0 25 0 1 0 1854979664 827011072 177600 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 201907 177600 145 145 0 201762 0
[pid=15256] vsize: 807628
Current children cumulated CPU time (s) 881.87
Current children cumulated vsize (Kb) 809752

[startup+900.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243520 0 0 0 88283 904 0 0 25 0 1 0 1854979664 827011072 177600 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 201907 177600 145 145 0 201762 0
[pid=15256] vsize: 807628
Current children cumulated CPU time (s) 891.87
Current children cumulated vsize (Kb) 809752

[startup+910.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243556 0 0 0 89283 905 0 0 25 0 1 0 1854979664 827158528 177636 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 201943 177636 145 145 0 201798 0
[pid=15256] vsize: 807772
Current children cumulated CPU time (s) 901.88
Current children cumulated vsize (Kb) 809896

[startup+920.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243556 0 0 0 90283 905 0 0 25 0 1 0 1854979664 827158528 177636 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 201943 177636 145 145 0 201798 0
[pid=15256] vsize: 807772
Current children cumulated CPU time (s) 911.88
Current children cumulated vsize (Kb) 809896

[startup+930.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243575 0 0 0 91283 905 0 0 25 0 1 0 1854979664 827236352 177655 4294967295 134512640 135094434 3221224432 3221223100 134550364 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 201962 177655 145 145 0 201817 0
[pid=15256] vsize: 807848
Current children cumulated CPU time (s) 921.88
Current children cumulated vsize (Kb) 809972

[startup+940.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243584 0 0 0 92283 905 0 0 25 0 1 0 1854979664 827273216 177664 4294967295 134512640 135094434 3221224432 3221223044 134563069 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 201971 177664 145 145 0 201826 0
[pid=15256] vsize: 807884
Current children cumulated CPU time (s) 931.88
Current children cumulated vsize (Kb) 810008

[startup+950.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243610 0 0 0 93283 905 0 0 25 0 1 0 1854979664 827379712 177690 4294967295 134512640 135094434 3221224432 3221223136 134559005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 201997 177690 145 145 0 201852 0
[pid=15256] vsize: 807988
Current children cumulated CPU time (s) 941.88
Current children cumulated vsize (Kb) 810112

[startup+960.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243610 0 0 0 94283 905 0 0 25 0 1 0 1854979664 827379712 177690 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 201997 177690 145 145 0 201852 0
[pid=15256] vsize: 807988
Current children cumulated CPU time (s) 951.88
Current children cumulated vsize (Kb) 810112

[startup+970.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243628 0 0 0 95283 905 0 0 25 0 1 0 1854979664 827453440 177708 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 202015 177708 145 145 0 201870 0
[pid=15256] vsize: 808060
Current children cumulated CPU time (s) 961.88
Current children cumulated vsize (Kb) 810184

[startup+980.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243666 0 0 0 96282 905 0 0 25 0 1 0 1854979664 827609088 177746 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 202053 177746 145 145 0 201908 0
[pid=15256] vsize: 808212
Current children cumulated CPU time (s) 971.87
Current children cumulated vsize (Kb) 810336

[startup+990.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243676 0 0 0 97282 906 0 0 25 0 1 0 1854979664 827650048 177756 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 202063 177756 145 145 0 201918 0
[pid=15256] vsize: 808252
Current children cumulated CPU time (s) 981.88
Current children cumulated vsize (Kb) 810376

[startup+1000.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243696 0 0 0 98282 906 0 0 25 0 1 0 1854979664 827727872 177776 4294967295 134512640 135094434 3221224432 3221223116 134553432 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 202082 177776 145 145 0 201937 0
[pid=15256] vsize: 808328
Current children cumulated CPU time (s) 991.88
Current children cumulated vsize (Kb) 810452

[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243721 0 0 0 99281 906 0 0 25 0 1 0 1854979664 827830272 177801 4294967295 134512640 135094434 3221224432 3221223044 134563089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 202107 177801 145 145 0 201962 0
[pid=15256] vsize: 808428
Current children cumulated CPU time (s) 1001.87
Current children cumulated vsize (Kb) 810552

[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243732 0 0 0 100281 906 0 0 25 0 1 0 1854979664 827875328 177812 4294967295 134512640 135094434 3221224432 3221223100 134553438 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 202118 177812 145 145 0 201973 0
[pid=15256] vsize: 808472
Current children cumulated CPU time (s) 1011.87
Current children cumulated vsize (Kb) 810596

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243751 0 0 0 101281 906 0 0 25 0 1 0 1854979664 827953152 177831 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 202137 177831 145 145 0 201992 0
[pid=15256] vsize: 808548
Current children cumulated CPU time (s) 1021.87
Current children cumulated vsize (Kb) 810672

[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243784 0 0 0 102281 907 0 0 25 0 1 0 1854979664 828088320 177864 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 202170 177864 145 145 0 202025 0
[pid=15256] vsize: 808680
Current children cumulated CPU time (s) 1031.88
Current children cumulated vsize (Kb) 810804

[startup+1050.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243785 0 0 0 103281 907 0 0 25 0 1 0 1854979664 828092416 177865 4294967295 134512640 135094434 3221224432 3221223092 134553494 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 202171 177865 145 145 0 202026 0
[pid=15256] vsize: 808684
Current children cumulated CPU time (s) 1041.88
Current children cumulated vsize (Kb) 810808

[startup+1060.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243803 0 0 0 104280 907 0 0 25 0 1 0 1854979664 828166144 177883 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 202189 177883 145 145 0 202044 0
[pid=15256] vsize: 808756
Current children cumulated CPU time (s) 1051.87
Current children cumulated vsize (Kb) 810880

[startup+1070.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243835 0 0 0 105280 907 0 0 25 0 1 0 1854979664 828297216 177915 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 202221 177915 145 145 0 202076 0
[pid=15256] vsize: 808884
Current children cumulated CPU time (s) 1061.87
Current children cumulated vsize (Kb) 811008

[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243846 0 0 0 106280 907 0 0 25 0 1 0 1854979664 828342272 177926 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 202232 177926 145 145 0 202087 0
[pid=15256] vsize: 808928
Current children cumulated CPU time (s) 1071.87
Current children cumulated vsize (Kb) 811052

[startup+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243846 0 0 0 107280 907 0 0 25 0 1 0 1854979664 828342272 177926 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 202232 177926 145 145 0 202087 0
[pid=15256] vsize: 808928
Current children cumulated CPU time (s) 1081.87
Current children cumulated vsize (Kb) 811052

[startup+1100.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243860 0 0 0 108280 907 0 0 25 0 1 0 1854979664 828399616 177940 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 202246 177940 145 145 0 202101 0
[pid=15256] vsize: 808984
Current children cumulated CPU time (s) 1091.87
Current children cumulated vsize (Kb) 811108

[startup+1110.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243876 0 0 0 109280 908 0 0 25 0 1 0 1854979664 828465152 177956 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 202262 177956 145 145 0 202117 0
[pid=15256] vsize: 809048
Current children cumulated CPU time (s) 1101.88
Current children cumulated vsize (Kb) 811172

[startup+1120.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243908 0 0 0 110280 908 0 0 25 0 1 0 1854979664 828620800 177988 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 202300 177988 145 145 0 202155 0
[pid=15256] vsize: 809200
Current children cumulated CPU time (s) 1111.88
Current children cumulated vsize (Kb) 811324

[startup+1130.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 244008 0 0 0 111278 909 0 0 25 0 1 0 1854979664 829026304 178088 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 202399 178088 145 145 0 202254 0
[pid=15256] vsize: 809596
Current children cumulated CPU time (s) 1121.87
Current children cumulated vsize (Kb) 811720

[startup+1140.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 244095 0 0 0 112277 909 0 0 25 0 1 0 1854979664 829382656 178175 4294967295 134512640 135094434 3221224432 3221223092 134553487 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 202486 178175 145 145 0 202341 0
[pid=15256] vsize: 809944
Current children cumulated CPU time (s) 1131.86
Current children cumulated vsize (Kb) 812068

[startup+1150.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 244149 0 0 0 113276 910 0 0 25 0 1 0 1854979664 829603840 178229 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 202540 178229 145 145 0 202395 0
[pid=15256] vsize: 810160
Current children cumulated CPU time (s) 1141.86
Current children cumulated vsize (Kb) 812284

[startup+1160.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 244195 0 0 0 114275 910 0 0 25 0 1 0 1854979664 829853696 178275 4294967295 134512640 135094434 3221224432 3221223044 134563074 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 202601 178275 145 145 0 202456 0
[pid=15256] vsize: 810404
Current children cumulated CPU time (s) 1151.85
Current children cumulated vsize (Kb) 812528

[startup+1170.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 244381 0 0 0 115271 911 0 0 25 0 1 0 1854979664 830611456 178461 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 202786 178461 145 145 0 202641 0
[pid=15256] vsize: 811144
Current children cumulated CPU time (s) 1161.82
Current children cumulated vsize (Kb) 813268

[startup+1180.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 244444 0 0 0 116270 912 0 0 25 0 1 0 1854979664 830861312 178524 4294967295 134512640 135094434 3221224432 3221223024 134551967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 202847 178524 145 145 0 202702 0
[pid=15256] vsize: 811388
Current children cumulated CPU time (s) 1171.82
Current children cumulated vsize (Kb) 813512

[startup+1190.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 244559 0 0 0 117268 913 0 0 25 0 1 0 1854979664 831332352 178639 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 202962 178639 145 145 0 202817 0
[pid=15256] vsize: 811848
Current children cumulated CPU time (s) 1181.81
Current children cumulated vsize (Kb) 813972

[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 244685 0 0 0 118266 914 0 0 25 0 1 0 1854979664 831836160 178765 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 203085 178765 145 145 0 202940 0
[pid=15256] vsize: 812340
Current children cumulated CPU time (s) 1191.8
Current children cumulated vsize (Kb) 814464

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 244876 0 0 0 119263 915 0 0 25 0 1 0 1854979664 832614400 178956 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 203275 178956 145 145 0 203130 0
[pid=15256] vsize: 813100
Current children cumulated CPU time (s) 1201.78
Current children cumulated vsize (Kb) 815224



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15256
Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15252/statm): 531 226 485 147 0 384 0
[pid=15252] vsize: 2124
Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 244876 0 0 0 119263 915 0 0 25 0 1 0 1854979664 832614400 178956 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15256/statm): 203275 178956 145 145 0 203130 0
[pid=15256] vsize: 813100
Current children cumulated CPU time (s) 1201.78
Current children cumulated vsize (Kb) 815224

Sending SIGTERM to -15252
Sleeping 2 seconds
One traced child (pid=15252) ended because it received signal 15 (SIGTERM)
One traced child (pid=15256) exited with status: 0
All traced children have exited ! Game is over.

Child status: 0
Real time (s): 1210.45
CPU time (s): 1202.14
CPU user time (s): 1192.63
CPU system time (s): 9.50855
CPU usage (%): 99.3138
Max. virtual memory (cumulated for all children) (Kb): 815224

Verifier Data

ERROR: no interpretation found !