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/MIPLIB/miplib2003/normalized-mps-v2-13-7-t1717.opb
MD5SUMbc46e72682d969c09e6f4028df473a45
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 201342
Optimality of the best value was proved NO
Number of terms in the objective function 73885
Biggest coefficient in the objective function 4066
Number of bits for the biggest coefficient in the objective function 12
Sum of the numbers in the objective function 172074995
Number of bits of the sum of numbers in the objective function 28
Biggest number in a constraint 4066
Number of bits of the biggest number in a constraint 12
Biggest sum of numbers in a constraint 172074995
Number of bits of the biggest sum of numbers28
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1189.2
Number of variables73885
Total number of constraints74436
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)74436
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint612

Trace number 6166

Launcher Data

LAUNCH ON wulflinc21 THE 2005-09-20 04:00:54 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3330 boxname=wulflinc21 idbench=986 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  bc46e72682d969c09e6f4028df473a45  /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-t1717.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-t1717.opb
IDLAUNCH: 3330
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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.161
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:        824640 kB
Buffers:         31208 kB
Cached:         148432 kB
SwapCached:        832 kB
Active:          67156 kB
Inactive:       115128 kB
HighTotal:      131008 kB
HighFree:        11144 kB
LowTotal:       903652 kB
LowFree:        813496 kB
SwapTotal:     2097892 kB
SwapFree:      2096456 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5776 kB
Slab:            22096 kB
Committed_AS:    64368 kB
PageTables:        340 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 04:21:04 (client local time) WITH STATUS 0 IN 1207.24 SECONDS
stats: 3330 7 1207.24 0

Solver Data

c Parsing PB file...
c Converting 1102 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #######################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[1100]---> BDD-cost: 1179
c ---[1098]---> BDD-cost: 1181
c ---[1096]---> BDD-cost: 1169
c ---[1094]---> BDD-cost: 1171
c ---[1092]---> BDD-cost: 1183
c ---[1090]---> BDD-cost: 1167
c ---[1088]---> BDD-cost: 1169
c ---[1086]---> BDD-cost: 1181
c ---[1084]---> BDD-cost: 1177
c ---[1082]---> BDD-cost: 1175
c ---[1080]---> BDD-cost: 1183
c ---[1078]---> BDD-cost: 1179
c ---[1076]---> BDD-cost: 1175
c ---[1074]---> BDD-cost: 1171
c ---[1072]---> BDD-cost: 1167
c ---[1070]---> BDD-cost: 1169
c ---[1068]---> BDD-cost: 1167
c ---[1066]---> BDD-cost: 1189
c ---[1064]---> BDD-cost: 1167
c ---[1062]---> BDD-cost: 1169
c ---[1060]---> BDD-cost: 1179
c ---[1058]---> BDD-cost: 1173
c ---[1056]---> BDD-cost: 1215
c ---[1054]---> BDD-cost: 1167
c ---[1052]---> BDD-cost: 1179
c ---[1050]---> BDD-cost: 1173
c ---[1048]---> BDD-cost: 1181
c ---[1046]---> BDD-cost: 1191
c ---[1044]---> BDD-cost: 1175
c ---[1042]---> BDD-cost: 1173
c ---[1040]---> BDD-cost: 1171
c ---[1038]---> BDD-cost: 1177
c ---[1036]---> BDD-cost: 1169
c ---[1034]---> BDD-cost: 1169
c ---[1032]---> BDD-cost: 1187
c ---[1030]---> BDD-cost: 1187
c ---[1028]---> BDD-cost: 1169
c ---[1026]---> BDD-cost: 1175
c ---[1024]---> BDD-cost: 1179
c ---[1022]---> BDD-cost: 1177
c ---[1020]---> BDD-cost: 1171
c ---[1018]---> BDD-cost: 1175
c ---[1016]---> BDD-cost: 1187
c ---[1014]---> BDD-cost: 1179
c ---[1012]---> BDD-cost: 1187
c ---[1010]---> BDD-cost: 1169
c ---[1008]---> BDD-cost: 1183
c ---[1006]---> BDD-cost: 1185
c ---[1004]---> BDD-cost: 1175
c ---[1002]---> BDD-cost: 1179
c ---[1000]---> BDD-cost: 1181
c ---[ 998]---> BDD-cost: 1155
c ---[ 996]---> BDD-cost: 1203
c ---[ 994]---> BDD-cost: 1191
c ---[ 992]---> BDD-cost: 1189
c ---[ 990]---> BDD-cost: 1175
c ---[ 988]---> BDD-cost: 1171
c ---[ 986]---> BDD-cost: 1191
c ---[ 984]---> BDD-cost: 1169
c ---[ 982]---> BDD-cost: 1187
c ---[ 980]---> BDD-cost: 1027
c ---[ 978]---> BDD-cost: 1175
c ---[ 976]---> BDD-cost: 1039
c ---[ 974]---> BDD-cost: 1185
c ---[ 972]---> BDD-cost: 1177
c ---[ 970]---> BDD-cost: 1167
c ---[ 968]---> BDD-cost: 1175
c ---[ 966]---> BDD-cost: 1171
c ---[ 964]---> BDD-cost: 1171
c ---[ 962]---> BDD-cost: 1175
c ---[ 960]---> BDD-cost: 1193
c ---[ 958]---> BDD-cost: 1171
c ---[ 956]---> BDD-cost: 1193
c ---[ 954]---> BDD-cost: 1175
c ---[ 952]---> BDD-cost: 1029
c ---[ 950]---> BDD-cost: 1193
c ---[ 948]---> BDD-cost: 1103
c ---[ 946]---> BDD-cost: 1171
c ---[ 944]---> BDD-cost: 1189
c ---[ 942]---> BDD-cost: 1179
c ---[ 940]---> BDD-cost: 1191
c ---[ 938]---> BDD-cost: 1003
c ---[ 936]---> BDD-cost: 1171
c ---[ 934]---> BDD-cost: 1171
c ---[ 932]---> BDD-cost: 1213
c ---[ 930]---> BDD-cost: 1175
c ---[ 928]---> BDD-cost: 1181
c ---[ 926]---> BDD-cost: 1173
c ---[ 924]---> BDD-cost: 1179
c ---[ 922]---> BDD-cost: 1179
c ---[ 920]---> BDD-cost: 1175
c ---[ 918]---> BDD-cost:  989
c ---[ 916]---> BDD-cost: 1187
c ---[ 914]---> BDD-cost: 1025
c ---[ 912]---> BDD-cost: 1141
c ---[ 910]---> BDD-cost: 1167
c ---[ 908]---> BDD-cost: 1115
c ---[ 906]---> BDD-cost: 1187
c ---[ 904]---> BDD-cost: 1117
c ---[ 902]---> BDD-cost: 1075
c ---[ 900]---> BDD-cost: 1167
c ---[ 898]---> BDD-cost: 1017
c ---[ 896]---> BDD-cost: 1079
c ---[ 894]---> BDD-cost: 1179
c ---[ 892]---> BDD-cost: 1191
c ---[ 890]---> BDD-cost: 1181
c ---[ 888]---> BDD-cost: 1171
c ---[ 886]---> BDD-cost: 1189
c ---[ 884]---> BDD-cost: 1177
c ---[ 882]---> BDD-cost: 1159
c ---[ 880]---> BDD-cost: 1181
c ---[ 878]---> BDD-cost: 1169
c ---[ 876]---> BDD-cost: 1167
c ---[ 874]---> BDD-cost: 1027
c ---[ 872]---> BDD-cost: 1093
c ---[ 870]---> BDD-cost: 1195
c ---[ 868]---> BDD-cost: 1169
c ---[ 866]---> BDD-cost: 1173
c ---[ 864]---> BDD-cost: 1171
c ---[ 862]---> BDD-cost: 1151
c ---[ 860]---> BDD-cost: 1173
c ---[ 858]---> BDD-cost: 1155
c ---[ 856]---> BDD-cost: 1173
c ---[ 854]---> BDD-cost: 1171
c ---[ 852]---> BDD-cost: 1145
c ---[ 850]---> BDD-cost: 1177
c ---[ 848]---> BDD-cost: 1179
c ---[ 846]---> BDD-cost: 1173
c ---[ 844]---> BDD-cost: 1173
c ---[ 842]---> BDD-cost: 1173
c ---[ 840]---> BDD-cost: 1187
c ---[ 838]---> BDD-cost: 1169
c ---[ 836]---> BDD-cost: 1055
c ---[ 834]---> BDD-cost: 1121
c ---[ 832]---> BDD-cost: 1171
c ---[ 830]---> BDD-cost: 1173
c ---[ 828]---> BDD-cost: 1177
c ---[ 826]---> BDD-cost: 1169
c ---[ 824]---> BDD-cost: 1171
c ---[ 822]---> BDD-cost: 1173
c ---[ 820]---> BDD-cost: 1169
c ---[ 818]---> BDD-cost: 1201
c ---[ 816]---> BDD-cost: 1173
c ---[ 814]---> BDD-cost: 1097
c ---[ 812]---> BDD-cost: 1171
c ---[ 810]---> BDD-cost: 1161
c ---[ 808]---> BDD-cost: 1187
c ---[ 806]---> BDD-cost: 1131
c ---[ 804]---> BDD-cost: 1173
c ---[ 802]---> BDD-cost: 1175
c ---[ 800]---> BDD-cost: 1171
c ---[ 798]---> BDD-cost: 1171
c ---[ 796]---> BDD-cost: 1169
c ---[ 794]---> BDD-cost: 1169
c ---[ 792]---> BDD-cost: 1165
c ---[ 790]---> BDD-cost: 1177
c ---[ 788]---> BDD-cost: 1157
c ---[ 786]---> BDD-cost: 1179
c ---[ 784]---> BDD-cost: 1129
c ---[ 782]---> BDD-cost: 1173
c ---[ 780]---> BDD-cost: 1175
c ---[ 778]---> BDD-cost: 1179
c ---[ 776]---> BDD-cost: 1173
c ---[ 774]---> BDD-cost: 1115
c ---[ 772]---> BDD-cost: 1071
c ---[ 770]---> BDD-cost: 1167
c ---[ 768]---> BDD-cost: 1187
c ---[ 766]---> BDD-cost: 1173
c ---[ 764]---> BDD-cost: 1091
c ---[ 762]---> BDD-cost: 1169
c ---[ 760]---> BDD-cost: 1025
c ---[ 758]---> BDD-cost: 1073
c ---[ 756]---> BDD-cost: 1167
c ---[ 754]---> BDD-cost: 1077
c ---[ 752]---> BDD-cost: 1197
c ---[ 750]---> BDD-cost: 1189
c ---[ 748]---> BDD-cost: 1197
c ---[ 746]---> BDD-cost: 1131
c ---[ 744]---> BDD-cost: 1115
c ---[ 742]---> BDD-cost: 1189
c ---[ 740]---> BDD-cost: 1177
c ---[ 738]---> BDD-cost: 1167
c ---[ 736]---> BDD-cost: 1175
c ---[ 734]---> BDD-cost: 1181
c ---[ 732]---> BDD-cost: 1171
c ---[ 730]---> BDD-cost: 1171
c ---[ 728]---> BDD-cost: 1189
c ---[ 726]---> BDD-cost: 1191
c ---[ 724]---> BDD-cost: 1103
c ---[ 722]---> BDD-cost: 1183
c ---[ 720]---> BDD-cost: 1151
c ---[ 718]---> BDD-cost: 1103
c ---[ 716]---> BDD-cost: 1171
c ---[ 714]---> BDD-cost: 1183
c ---[ 712]---> BDD-cost: 1171
c ---[ 710]---> BDD-cost: 1179
c ---[ 708]---> BDD-cost: 1173
c ---[ 706]---> BDD-cost: 1073
c ---[ 704]---> BDD-cost: 1191
c ---[ 702]---> BDD-cost: 1175
c ---[ 700]---> BDD-cost: 1139
c ---[ 698]---> BDD-cost: 1171
c ---[ 696]---> BDD-cost: 1173
c ---[ 694]---> BDD-cost: 1163
c ---[ 692]---> BDD-cost: 1173
c ---[ 690]---> BDD-cost: 1175
c ---[ 688]---> BDD-cost: 1189
c ---[ 686]---> BDD-cost: 1173
c ---[ 684]---> BDD-cost: 1173
c ---[ 682]---> BDD-cost: 1071
c ---[ 680]---> BDD-cost: 1179
c ---[ 678]---> BDD-cost: 1125
c ---[ 676]---> BDD-cost: 1171
c ---[ 674]---> BDD-cost: 1057
c ---[ 672]---> BDD-cost: 1189
c ---[ 670]---> BDD-cost: 1107
c ---[ 668]---> BDD-cost: 1159
c ---[ 666]---> BDD-cost: 1175
c ---[ 664]---> BDD-cost: 1063
c ---[ 662]---> BDD-cost: 1173
c ---[ 660]---> BDD-cost: 1171
c ---[ 658]---> BDD-cost: 1171
c ---[ 656]---> BDD-cost: 1165
c ---[ 654]---> BDD-cost: 1165
c ---[ 652]---> BDD-cost: 1171
c ---[ 650]---> BDD-cost: 1077
c ---[ 648]---> BDD-cost: 1069
c ---[ 646]---> BDD-cost: 1175
c ---[ 644]---> BDD-cost: 1159
c ---[ 642]---> BDD-cost: 1097
c ---[ 640]---> BDD-cost: 1175
c ---[ 638]---> BDD-cost:  859
c ---[ 636]---> BDD-cost: 1173
c ---[ 634]---> BDD-cost: 1169
c ---[ 632]---> BDD-cost: 1173
c ---[ 630]---> BDD-cost: 1097
c ---[ 628]---> BDD-cost: 1161
c ---[ 626]---> BDD-cost: 1157
c ---[ 624]---> BDD-cost: 1165
c ---[ 622]---> BDD-cost: 1185
c ---[ 620]---> BDD-cost: 1179
c ---[ 618]---> BDD-cost: 1155
c ---[ 616]---> BDD-cost: 1167
c ---[ 614]---> BDD-cost: 1181
c ---[ 612]---> BDD-cost: 1121
c ---[ 610]---> BDD-cost: 1121
c ---[ 608]---> BDD-cost:  963
c ---[ 606]---> BDD-cost: 1173
c ---[ 604]---> BDD-cost: 1151
c ---[ 602]---> BDD-cost: 1177
c ---[ 600]---> BDD-cost: 1191
c ---[ 598]---> BDD-cost: 1187
c ---[ 596]---> BDD-cost: 1051
c ---[ 594]---> BDD-cost:  987
c ---[ 592]---> BDD-cost: 1173
c ---[ 590]---> BDD-cost: 1175
c ---[ 588]---> BDD-cost: 1173
c ---[ 586]---> BDD-cost: 1121
c ---[ 584]---> BDD-cost: 1157
c ---[ 582]---> BDD-cost: 1173
c ---[ 580]---> BDD-cost: 1175
c ---[ 578]---> BDD-cost: 1181
c ---[ 576]---> BDD-cost: 1079
c ---[ 574]---> BDD-cost:  983
c ---[ 572]---> BDD-cost:  879
c ---[ 570]---> BDD-cost: 1169
c ---[ 568]---> BDD-cost: 1181
c ---[ 566]---> BDD-cost: 1169
c ---[ 564]---> BDD-cost: 1185
c ---[ 562]---> BDD-cost: 1177
c ---[ 560]---> BDD-cost: 1159
c ---[ 558]---> BDD-cost: 1153
c ---[ 556]---> BDD-cost: 1173
c ---[ 554]---> BDD-cost: 1191
c ---[ 552]---> BDD-cost: 1177
c ---[ 550]---> BDD-cost: 1175
c ---[ 548]---> BDD-cost:  887
c ---[ 546]---> BDD-cost: 1191
c ---[ 544]---> BDD-cost: 1155
c ---[ 542]---> BDD-cost: 1169
c ---[ 540]---> BDD-cost: 1127
c ---[ 538]---> BDD-cost: 1179
c ---[ 536]---> BDD-cost: 1189
c ---[ 534]---> BDD-cost: 1171
c ---[ 532]---> BDD-cost: 1167
c ---[ 530]---> BDD-cost: 1171
c ---[ 528]---> BDD-cost: 1175
c ---[ 526]---> BDD-cost:  885
c ---[ 524]---> BDD-cost: 1183
c ---[ 522]---> BDD-cost: 1175
c ---[ 520]---> BDD-cost: 1193
c ---[ 518]---> BDD-cost: 1181
c ---[ 516]---> BDD-cost: 1169
c ---[ 514]---> BDD-cost: 1181
c ---[ 512]---> BDD-cost: 1169
c ---[ 510]---> BDD-cost: 1177
c ---[ 508]---> BDD-cost: 1171
c ---[ 506]---> BDD-cost: 1169
c ---[ 504]---> BDD-cost: 1179
c ---[ 502]---> BDD-cost: 1183
c ---[ 500]---> BDD-cost: 1165
c ---[ 498]---> BDD-cost: 1163
c ---[ 496]---> BDD-cost: 1189
c ---[ 494]---> BDD-cost: 1181
c ---[ 492]---> BDD-cost: 1171
c ---[ 490]---> BDD-cost: 1171
c ---[ 488]---> BDD-cost: 1173
c ---[ 486]---> BDD-cost: 1171
c ---[ 484]---> BDD-cost: 1171
c ---[ 482]---> BDD-cost: 1175
c ---[ 480]---> BDD-cost: 1171
c ---[ 478]---> BDD-cost: 1141
c ---[ 476]---> BDD-cost: 1185
c ---[ 474]---> BDD-cost: 1167
c ---[ 472]---> BDD-cost: 1179
c ---[ 470]---> BDD-cost: 1175
c ---[ 468]---> BDD-cost: 1177
c ---[ 466]---> BDD-cost:  775
c ---[ 464]---> BDD-cost: 1191
c ---[ 462]---> BDD-cost: 1207
c ---[ 460]---> BDD-cost: 1179
c ---[ 458]---> BDD-cost: 1149
c ---[ 456]---> BDD-cost: 1183
c ---[ 454]---> BDD-cost:  787
c ---[ 452]---> BDD-cost: 1173
c ---[ 450]---> BDD-cost: 1169
c ---[ 448]---> BDD-cost: 1131
c ---[ 446]---> BDD-cost: 1129
c ---[ 444]---> BDD-cost: 1167
c ---[ 442]---> BDD-cost: 1177
c ---[ 440]---> BDD-cost: 1185
c ---[ 438]---> BDD-cost: 1185
c ---[ 436]---> BDD-cost: 1189
c ---[ 434]---> BDD-cost: 1169
c ---[ 432]---> BDD-cost: 1113
c ---[ 430]---> BDD-cost: 1167
c ---[ 428]---> BDD-cost: 1181
c ---[ 426]---> BDD-cost: 1171
c ---[ 424]---> BDD-cost: 1191
c ---[ 422]---> BDD-cost: 1181
c ---[ 420]---> BDD-cost: 1169
c ---[ 418]---> BDD-cost: 1137
c ---[ 416]---> BDD-cost: 1159
c ---[ 414]---> BDD-cost: 1169
c ---[ 412]---> BDD-cost: 1175
c ---[ 410]---> BDD-cost: 1167
c ---[ 408]---> BDD-cost: 1195
c ---[ 406]---> BDD-cost: 1169
c ---[ 404]---> BDD-cost: 1171
c ---[ 402]---> BDD-cost: 1177
c ---[ 400]---> BDD-cost: 1147
c ---[ 398]---> BDD-cost: 1171
c ---[ 396]---> BDD-cost: 1173
c ---[ 394]---> BDD-cost:  723
c ---[ 392]---> BDD-cost: 1173
c ---[ 390]---> BDD-cost: 1177
c ---[ 388]---> BDD-cost: 1169
c ---[ 386]---> BDD-cost: 1187
c ---[ 384]---> BDD-cost: 1209
c ---[ 382]---> BDD-cost: 1171
c ---[ 380]---> BDD-cost: 1181
c ---[ 378]---> BDD-cost: 1197
c ---[ 376]---> BDD-cost: 1183
c ---[ 374]---> BDD-cost: 1175
c ---[ 372]---> BDD-cost: 1165
c ---[ 370]---> BDD-cost: 1175
c ---[ 368]---> BDD-cost: 1175
c ---[ 366]---> BDD-cost: 1177
c ---[ 364]---> BDD-cost: 1179
c ---[ 362]---> BDD-cost: 1173
c ---[ 360]---> BDD-cost: 1169
c ---[ 358]---> BDD-cost: 1173
c ---[ 356]---> BDD-cost: 1173
c ---[ 354]---> BDD-cost: 1171
c ---[ 352]---> BDD-cost: 1177
c ---[ 350]---> BDD-cost: 1169
c ---[ 348]---> BDD-cost: 1185
c ---[ 346]---> BDD-cost: 1173
c ---[ 344]---> BDD-cost: 1103
c ---[ 342]---> BDD-cost: 1179
c ---[ 340]---> BDD-cost: 1173
c ---[ 338]---> BDD-cost: 1221
c ---[ 336]---> BDD-cost: 1177
c ---[ 334]---> BDD-cost: 1183
c ---[ 332]---> BDD-cost: 1179
c ---[ 330]---> BDD-cost: 1171
c ---[ 328]---> BDD-cost: 1175
c ---[ 326]---> BDD-cost: 1173
c ---[ 324]---> BDD-cost: 1175
c ---[ 322]---> BDD-cost: 1099
c ---[ 320]---> BDD-cost: 1203
c ---[ 318]---> BDD-cost: 1171
c ---[ 316]---> BDD-cost: 1165
c ---[ 314]---> BDD-cost: 1177
c ---[ 312]---> BDD-cost: 1169
c ---[ 310]---> BDD-cost: 1175
c ---[ 308]---> BDD-cost: 1173
c ---[ 306]---> BDD-cost: 1173
c ---[ 304]---> BDD-cost: 1183
c ---[ 302]---> BDD-cost: 1175
c ---[ 300]---> BDD-cost: 1165
c ---[ 298]---> BDD-cost: 1175
c ---[ 296]---> BDD-cost: 1153
c ---[ 294]---> BDD-cost: 1153
c ---[ 292]---> BDD-cost: 1175
c ---[ 290]---> BDD-cost: 1173
c ---[ 288]---> BDD-cost:  735
c ---[ 286]---> BDD-cost: 1179
c ---[ 284]---> BDD-cost: 1157
c ---[ 282]---> BDD-cost: 1183
c ---[ 280]---> BDD-cost: 1179
c ---[ 278]---> BDD-cost: 1181
c ---[ 276]---> BDD-cost: 1175
c ---[ 274]---> BDD-cost: 1181
c ---[ 272]---> BDD-cost: 1185
c ---[ 270]---> BDD-cost: 1161
c ---[ 268]---> BDD-cost: 1177
c ---[ 266]---> BDD-cost: 1165
c ---[ 264]---> BDD-cost: 1161
c ---[ 262]---> BDD-cost: 1065
c ---[ 260]---> BDD-cost: 1171
c ---[ 258]---> BDD-cost: 1189
c ---[ 256]---> BDD-cost: 1163
c ---[ 254]---> BDD-cost: 1177
c ---[ 252]---> BDD-cost: 1179
c ---[ 250]---> BDD-cost: 1187
c ---[ 248]---> BDD-cost: 1143
c ---[ 246]---> BDD-cost: 1183
c ---[ 244]---> BDD-cost: 1153
c ---[ 242]---> BDD-cost: 1177
c ---[ 240]---> BDD-cost: 1173
c ---[ 238]---> BDD-cost: 1177
c ---[ 236]---> BDD-cost: 1171
c ---[ 234]---> BDD-cost: 1103
c ---[ 232]---> BDD-cost: 1173
c ---[ 230]---> BDD-cost: 1175
c ---[ 228]---> BDD-cost: 1123
c ---[ 226]---> BDD-cost: 1169
c ---[ 224]---> BDD-cost: 1187
c ---[ 222]---> BDD-cost: 1101
c ---[ 220]---> BDD-cost: 1165
c ---[ 218]---> BDD-cost: 1193
c ---[ 216]---> BDD-cost: 1179
c ---[ 214]---> BDD-cost: 1177
c ---[ 212]---> BDD-cost: 1173
c ---[ 210]---> BDD-cost: 1173
c ---[ 208]---> BDD-cost: 1153
c ---[ 206]---> BDD-cost: 1183
c ---[ 204]---> BDD-cost: 1181
c ---[ 202]---> BDD-cost: 1179
c ---[ 200]---> BDD-cost: 1181
c ---[ 198]---> BDD-cost: 1181
c ---[ 196]---> BDD-cost: 1173
c ---[ 194]---> BDD-cost: 1173
c ---[ 192]---> BDD-cost: 1173
c ---[ 190]---> BDD-cost: 1185
c ---[ 188]---> BDD-cost: 1165
c ---[ 186]---> BDD-cost: 1173
c ---[ 184]---> BDD-cost: 1169
c ---[ 182]---> BDD-cost: 1183
c ---[ 180]---> BDD-cost: 1189
c ---[ 178]---> BDD-cost: 1177
c ---[ 176]---> BDD-cost: 1181
c ---[ 174]---> BDD-cost: 1173
c ---[ 172]---> BDD-cost: 1193
c ---[ 170]---> BDD-cost: 1173
c ---[ 168]---> BDD-cost: 1187
c ---[ 166]---> BDD-cost: 1193
c ---[ 164]---> BDD-cost: 1183
c ---[ 162]---> BDD-cost: 1175
c ---[ 160]---> BDD-cost: 1137
c ---[ 158]---> BDD-cost: 1185
c ---[ 156]---> BDD-cost: 1097
c ---[ 154]---> BDD-cost: 1195
c ---[ 152]---> BDD-cost: 1175
c ---[ 150]---> BDD-cost: 1175
c ---[ 148]---> BDD-cost: 1187
c ---[ 146]---> BDD-cost: 1179
c ---[ 144]---> BDD-cost: 1167
c ---[ 142]---> BDD-cost: 1175
c ---[ 140]---> BDD-cost: 1173
c ---[ 138]---> BDD-cost: 1173
c ---[ 136]---> BDD-cost: 1171
c ---[ 134]---> BDD-cost: 1179
c ---[ 132]---> BDD-cost: 1165
c ---[ 130]---> BDD-cost: 1165
c ---[ 128]---> BDD-cost: 1145
c ---[ 126]---> BDD-cost: 1179
c ---[ 124]---> BDD-cost: 1193
c ---[ 122]---> BDD-cost: 1175
c ---[ 120]---> BDD-cost: 1177
c ---[ 118]---> BDD-cost: 1181
c ---[ 116]---> BDD-cost: 1181
c ---[ 114]---> BDD-cost: 1195
c ---[ 112]---> BDD-cost: 1165
c ---[ 110]---> BDD-cost: 1169
c ---[ 108]---> BDD-cost: 1133
c ---[ 106]---> BDD-cost: 1199
c ---[ 104]---> BDD-cost: 1197
c ---[ 102]---> BDD-cost: 1177
c ---[ 100]---> BDD-cost: 1121
c ---[  98]---> BDD-cost: 1143
c ---[  96]---> BDD-cost: 1171
c ---[  94]---> BDD-cost: 1167
c ---[  92]---> BDD-cost: 1175
c ---[  90]---> BDD-cost: 1157
c ---[  88]---> BDD-cost: 1085
c ---[  86]---> BDD-cost: 1167
c ---[  84]---> BDD-cost: 1157
c ---[  82]---> BDD-cost: 1157
c ---[  80]---> BDD-cost: 1175
c ---[  78]---> BDD-cost: 1119
c ---[  76]---> BDD-cost: 1169
c ---[  74]---> BDD-cost: 1177
c ---[  72]---> BDD-cost: 1087
c ---[  70]---> BDD-cost: 1121
c ---[  68]---> BDD-cost: 1171
c ---[  66]---> BDD-cost: 1171
c ---[  64]---> BDD-cost: 1155
c ---[  62]---> BDD-cost: 1173
c ---[  60]---> BDD-cost: 1173
c ---[  58]---> BDD-cost: 1165
c ---[  56]---> BDD-cost: 1169
c ---[  54]---> BDD-cost: 1123
c ---[  52]---> BDD-cost: 1167
c ---[  50]---> BDD-cost: 1073
c ---[  48]---> BDD-cost: 1155
c ---[  46]---> BDD-cost: 1115
c ---[  44]---> BDD-cost: 1171
c ---[  42]---> BDD-cost: 1153
c ---[  40]---> BDD-cost: 1101
c ---[  38]---> BDD-cost: 1065
c ---[  36]---> BDD-cost: 1111
c ---[  34]---> BDD-cost: 1153
c ---[  32]---> BDD-cost: 1061
c ---[  30]---> BDD-cost: 1185
c ---[  28]---> BDD-cost: 1061
c ---[  26]---> BDD-cost: 1173
c ---[  24]---> BDD-cost: 1177
c ---[  22]---> BDD-cost: 1113
c ---[  20]---> BDD-cost: 1151
c ---[  18]---> BDD-cost: 1091
c ---[  16]---> BDD-cost: 1173
c ---[  14]---> BDD-cost: 1137
c ---[  12]---> BDD-cost: 1065
c ---[  10]---> BDD-cost: 1189
c ---[   8]---> BDD-cost: 1169
c ---[   6]---> BDD-cost: 1039
c ---[   4]---> BDD-cost: 1119
c ---[   2]---> BDD-cost: 1147
c ---[   0]---> BDD-cost: 1159
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 1593441  4143559 |  531147       0        0     nan |  0.000 % |
c |       100 | 1593441  4143559 |  584261     100     3100    31.0 |  0.077 % |
c |       250 | 1593441  4143559 |  642687     250    15023    60.1 |  0.077 % |
c |       475 | 1593441  4143559 |  706956     475    28709    60.4 |  0.077 % |
c |       812 | 1593441  4143559 |  777652     812    75062    92.4 |  0.077 % |
c |      1329 | 1593441  4143559 |  855417    1329   184901   139.1 |  0.077 % |
c |      2088 | 1593441  4143559 |  940959    2088   283938   136.0 |  0.077 % |
c |      3228 | 1593441  4143559 | 1035055    3228   516925   160.1 |  0.077 % |
c |      4939 | 1593441  4143559 | 1138560    4939   851066   172.3 |  0.077 % |
c |      7501 | 1593441  4143559 | 1252416    7501  1448612   193.1 |  0.077 % |
c |     11345 | 1593441  4143559 | 1377658   11345  2447772   215.8 |  0.077 % |
c |     17111 | 1593441  4143559 | 1515424   17111  3892289   227.5 |  0.077 % |
c |     25761 | 1593441  4143559 | 1666966   25761  5900360   229.0 |  0.077 % |

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/13383/stat): 13383 (minisat+_script) R 13382 13383 20602 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1732762749 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/13383/statm): 174 3 169 147 0 27 0
[pid=13383] 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=13384
New process pid=13385
New process pid=13386
execve syscall for /bin/sed executable
One traced child (pid=13385) 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=13386) exited with status: 0
One traced child (pid=13384) exited with status: 0
New process pid=13387
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-t1717.opb

[startup+10.0032 s]
Raw data (loadavg): 0.93 0.96 0.91 2/58 13389
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 13602 0 0 0 876 64 0 0 25 0 1 0 1732762754 56045568 12476 4294967295 134512640 135094434 3221224432 3221152064 134596869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13387/statm): 13683 12476 145 145 0 13538 0
[pid=13387] vsize: 54732
Current children cumulated CPU time (s) 9.41
Current children cumulated vsize (Kb) 56856

[startup+20.0049 s]
Raw data (loadavg): 0.94 0.96 0.91 1/58 13389
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) T 13383 13383 20602 0 -1 0 28946 0 0 0 1774 119 0 0 19 0 1 0 1732762754 133025792 27161 4294967295 134512640 135094434 3221224432 3221087964 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/13387/statm): 32477 27161 145 145 0 32332 0
[pid=13387] vsize: 129908
Current children cumulated CPU time (s) 18.94
Current children cumulated vsize (Kb) 132032

[startup+30.0056 s]
Raw data (loadavg): 0.95 0.96 0.91 2/58 13389
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 56733 0 0 0 2534 233 0 0 25 0 1 0 1732762754 259289088 54884 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13387/statm): 63303 54884 145 145 0 63158 0
[pid=13387] vsize: 253212
Current children cumulated CPU time (s) 27.68
Current children cumulated vsize (Kb) 255336

[startup+40.0063 s]
Raw data (loadavg): 0.96 0.96 0.91 2/58 13389
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 56937 0 0 0 3533 234 0 0 25 0 1 0 1732762754 259420160 55088 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13387/statm): 63335 55088 145 145 0 63190 0
[pid=13387] vsize: 253340
Current children cumulated CPU time (s) 37.68
Current children cumulated vsize (Kb) 255464

[startup+50.0079 s]
Raw data (loadavg): 0.96 0.96 0.91 2/58 13389
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 56990 0 0 0 4532 234 0 0 25 0 1 0 1732762754 259633152 55141 4294967295 134512640 135094434 3221224432 3221223024 134556961 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13387/statm): 63387 55141 145 145 0 63242 0
[pid=13387] vsize: 253548
Current children cumulated CPU time (s) 47.67
Current children cumulated vsize (Kb) 255672

[startup+60.0086 s]
Raw data (loadavg): 0.97 0.96 0.91 2/58 13389
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 57051 0 0 0 5531 235 0 0 25 0 1 0 1732762754 259887104 55202 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13387/statm): 63449 55202 145 145 0 63304 0
[pid=13387] vsize: 253796
Current children cumulated CPU time (s) 57.67
Current children cumulated vsize (Kb) 255920

[startup+70.0083 s]
Raw data (loadavg): 1.21 1.01 0.93 3/72 13406
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 57124 0 0 0 6528 236 0 0 25 0 1 0 1732762754 260182016 55275 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 63521 55275 145 145 0 63376 0
[pid=13387] vsize: 254084
Current children cumulated CPU time (s) 67.65
Current children cumulated vsize (Kb) 256208

[startup+80.0104 s]
Raw data (loadavg): 1.49 1.08 0.95 3/72 13406
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 57179 0 0 0 7527 237 0 0 25 0 1 0 1732762754 260407296 55330 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 63576 55330 145 145 0 63431 0
[pid=13387] vsize: 254304
Current children cumulated CPU time (s) 77.65
Current children cumulated vsize (Kb) 256428

[startup+90.0107 s]
Raw data (loadavg): 1.80 1.16 0.97 3/72 13406
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 57248 0 0 0 8525 238 0 0 25 0 1 0 1732762754 260694016 55399 4294967295 134512640 135094434 3221224432 3221223024 134556928 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 63646 55399 145 145 0 63501 0
[pid=13387] vsize: 254584
Current children cumulated CPU time (s) 87.64
Current children cumulated vsize (Kb) 256708

[startup+100.012 s]
Raw data (loadavg): 1.83 1.18 0.98 2/62 13632
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 57333 0 0 0 9518 241 0 0 25 0 1 0 1732762754 261046272 55484 4294967295 134512640 135094434 3221224432 3221223024 134556999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 63732 55484 145 145 0 63587 0
[pid=13387] vsize: 254928
Current children cumulated CPU time (s) 97.6
Current children cumulated vsize (Kb) 257052

[startup+110.022 s]
Raw data (loadavg): 1.86 1.21 1.00 2/64 13638
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 57414 0 0 0 10516 242 0 0 25 0 1 0 1732762754 261283840 55565 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 63790 55565 145 145 0 63645 0
[pid=13387] vsize: 255160
Current children cumulated CPU time (s) 107.59
Current children cumulated vsize (Kb) 257284

[startup+120.022 s]
Raw data (loadavg): 1.88 1.23 1.01 2/64 13650
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 57480 0 0 0 11514 243 0 0 25 0 1 0 1732762754 261550080 55631 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 63855 55631 145 145 0 63710 0
[pid=13387] vsize: 255420
Current children cumulated CPU time (s) 117.58
Current children cumulated vsize (Kb) 257544

[startup+130.022 s]
Raw data (loadavg): 1.82 1.24 1.01 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 57573 0 0 0 12511 244 0 0 25 0 1 0 1732762754 261935104 55724 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 63949 55724 145 145 0 63804 0
[pid=13387] vsize: 255796
Current children cumulated CPU time (s) 127.56
Current children cumulated vsize (Kb) 257920

[startup+140.023 s]
Raw data (loadavg): 1.69 1.23 1.01 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 57638 0 0 0 13511 245 0 0 25 0 1 0 1732762754 262209536 55789 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 64016 55789 145 145 0 63871 0
[pid=13387] vsize: 256064
Current children cumulated CPU time (s) 137.57
Current children cumulated vsize (Kb) 258188

[startup+150.024 s]
Raw data (loadavg): 1.58 1.23 1.01 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 57711 0 0 0 14510 245 0 0 25 0 1 0 1732762754 262508544 55862 4294967295 134512640 135094434 3221224432 3221223024 134556975 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 64089 55862 145 145 0 63944 0
[pid=13387] vsize: 256356
Current children cumulated CPU time (s) 147.56
Current children cumulated vsize (Kb) 258480

[startup+160.024 s]
Raw data (loadavg): 1.49 1.22 1.01 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 57798 0 0 0 15509 246 0 0 25 0 1 0 1732762754 262844416 55949 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 64171 55949 145 145 0 64026 0
[pid=13387] vsize: 256684
Current children cumulated CPU time (s) 157.56
Current children cumulated vsize (Kb) 258808

[startup+170.024 s]
Raw data (loadavg): 1.42 1.21 1.01 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 57853 0 0 0 16508 246 0 0 25 0 1 0 1732762754 263069696 56004 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 64226 56004 145 145 0 64081 0
[pid=13387] vsize: 256904
Current children cumulated CPU time (s) 167.55
Current children cumulated vsize (Kb) 259028

[startup+180.025 s]
Raw data (loadavg): 1.35 1.20 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 57948 0 0 0 17507 247 0 0 25 0 1 0 1732762754 263454720 56099 4294967295 134512640 135094434 3221224432 3221223024 134556961 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 64320 56099 145 145 0 64175 0
[pid=13387] vsize: 257280
Current children cumulated CPU time (s) 177.55
Current children cumulated vsize (Kb) 259404

[startup+190.024 s]
Raw data (loadavg): 1.30 1.20 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 58013 0 0 0 18506 247 0 0 25 0 1 0 1732762754 263716864 56164 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 64384 56164 145 145 0 64239 0
[pid=13387] vsize: 257536
Current children cumulated CPU time (s) 187.54
Current children cumulated vsize (Kb) 259660

[startup+200.025 s]
Raw data (loadavg): 1.25 1.19 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 58102 0 0 0 19504 248 0 0 25 0 1 0 1732762754 264081408 56253 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 64473 56253 145 145 0 64328 0
[pid=13387] vsize: 257892
Current children cumulated CPU time (s) 197.53
Current children cumulated vsize (Kb) 260016

[startup+210.026 s]
Raw data (loadavg): 1.21 1.18 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 58186 0 0 0 20504 249 0 0 25 0 1 0 1732762754 264421376 56337 4294967295 134512640 135094434 3221224432 3221223024 134556908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 64556 56337 145 145 0 64411 0
[pid=13387] vsize: 258224
Current children cumulated CPU time (s) 207.54
Current children cumulated vsize (Kb) 260348

[startup+220.027 s]
Raw data (loadavg): 1.18 1.18 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 58285 0 0 0 21503 249 0 0 25 0 1 0 1732762754 264822784 56436 4294967295 134512640 135094434 3221224432 3221223088 134561698 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 64654 56436 145 145 0 64509 0
[pid=13387] vsize: 258616
Current children cumulated CPU time (s) 217.53
Current children cumulated vsize (Kb) 260740

[startup+230.027 s]
Raw data (loadavg): 1.15 1.17 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 58363 0 0 0 22501 250 0 0 25 0 1 0 1732762754 265142272 56514 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 64732 56514 145 145 0 64587 0
[pid=13387] vsize: 258928
Current children cumulated CPU time (s) 227.52
Current children cumulated vsize (Kb) 261052

[startup+240.027 s]
Raw data (loadavg): 1.13 1.16 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 58426 0 0 0 23501 250 0 0 25 0 1 0 1732762754 265400320 56577 4294967295 134512640 135094434 3221224432 3221223072 134562057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 64795 56577 145 145 0 64650 0
[pid=13387] vsize: 259180
Current children cumulated CPU time (s) 237.52
Current children cumulated vsize (Kb) 261304

[startup+250.029 s]
Raw data (loadavg): 1.11 1.16 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 58499 0 0 0 24500 251 0 0 25 0 1 0 1732762754 265699328 56650 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 64868 56650 145 145 0 64723 0
[pid=13387] vsize: 259472
Current children cumulated CPU time (s) 247.52
Current children cumulated vsize (Kb) 261596

[startup+260.029 s]
Raw data (loadavg): 1.09 1.15 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 58566 0 0 0 25499 251 0 0 25 0 1 0 1732762754 266002432 56717 4294967295 134512640 135094434 3221224432 3221223088 134558420 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 64942 56717 145 145 0 64797 0
[pid=13387] vsize: 259768
Current children cumulated CPU time (s) 257.51
Current children cumulated vsize (Kb) 261892

[startup+270.029 s]
Raw data (loadavg): 1.08 1.15 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 58644 0 0 0 26498 252 0 0 25 0 1 0 1732762754 266326016 56795 4294967295 134512640 135094434 3221224432 3221223044 134562992 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 65021 56795 145 145 0 64876 0
[pid=13387] vsize: 260084
Current children cumulated CPU time (s) 267.51
Current children cumulated vsize (Kb) 262208

[startup+280.03 s]
Raw data (loadavg): 1.06 1.14 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 58736 0 0 0 27497 252 0 0 25 0 1 0 1732762754 266584064 56887 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 65084 56887 145 145 0 64939 0
[pid=13387] vsize: 260336
Current children cumulated CPU time (s) 277.5
Current children cumulated vsize (Kb) 262460

[startup+290.03 s]
Raw data (loadavg): 1.05 1.14 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 58828 0 0 0 28497 253 0 0 25 0 1 0 1732762754 266960896 56979 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 65176 56979 145 145 0 65031 0
[pid=13387] vsize: 260704
Current children cumulated CPU time (s) 287.51
Current children cumulated vsize (Kb) 262828

[startup+300.031 s]
Raw data (loadavg): 1.05 1.13 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 58924 0 0 0 29495 254 0 0 25 0 1 0 1732762754 267354112 57075 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 65272 57075 145 145 0 65127 0
[pid=13387] vsize: 261088
Current children cumulated CPU time (s) 297.5
Current children cumulated vsize (Kb) 263212

[startup+310.032 s]
Raw data (loadavg): 1.04 1.13 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 59019 0 0 0 30494 255 0 0 25 0 1 0 1732762754 267739136 57170 4294967295 134512640 135094434 3221224432 3221223068 134562980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 65366 57170 145 145 0 65221 0
[pid=13387] vsize: 261464
Current children cumulated CPU time (s) 307.5
Current children cumulated vsize (Kb) 263588

[startup+320.032 s]
Raw data (loadavg): 1.03 1.12 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 59153 0 0 0 31494 255 0 0 25 0 1 0 1732762754 268091392 57304 4294967295 134512640 135094434 3221224432 3221223104 134555298 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 65452 57304 145 145 0 65307 0
[pid=13387] vsize: 261808
Current children cumulated CPU time (s) 317.5
Current children cumulated vsize (Kb) 263932

[startup+330.033 s]
Raw data (loadavg): 1.03 1.12 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 59237 0 0 0 32492 256 0 0 25 0 1 0 1732762754 268427264 57388 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 65534 57388 145 145 0 65389 0
[pid=13387] vsize: 262136
Current children cumulated CPU time (s) 327.49
Current children cumulated vsize (Kb) 264260

[startup+340.034 s]
Raw data (loadavg): 1.02 1.11 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 59346 0 0 0 33491 256 0 0 25 0 1 0 1732762754 268877824 57497 4294967295 134512640 135094434 3221224432 3221223024 134556999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 65644 57497 145 145 0 65499 0
[pid=13387] vsize: 262576
Current children cumulated CPU time (s) 337.48
Current children cumulated vsize (Kb) 264700

[startup+350.034 s]
Raw data (loadavg): 1.02 1.11 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 59436 0 0 0 34490 257 0 0 25 0 1 0 1732762754 269242368 57587 4294967295 134512640 135094434 3221224432 3221223024 134556931 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 65733 57587 145 145 0 65588 0
[pid=13387] vsize: 262932
Current children cumulated CPU time (s) 347.48
Current children cumulated vsize (Kb) 265056

[startup+360.035 s]
Raw data (loadavg): 1.02 1.11 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 59544 0 0 0 35489 258 0 0 25 0 1 0 1732762754 269680640 57695 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13387/statm): 65840 57695 145 145 0 65695 0
[pid=13387] vsize: 263360
Current children cumulated CPU time (s) 357.48
Current children cumulated vsize (Kb) 265484

[startup+370.035 s]
Raw data (loadavg): 1.01 1.10 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 59654 0 0 0 36487 259 0 0 25 0 1 0 1732762754 270131200 57805 4294967295 134512640 135094434 3221224432 3221223044 134563077 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 65950 57805 145 145 0 65805 0
[pid=13387] vsize: 263800
Current children cumulated CPU time (s) 367.47
Current children cumulated vsize (Kb) 265924

[startup+380.035 s]
Raw data (loadavg): 1.01 1.10 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 59710 0 0 0 37486 260 0 0 25 0 1 0 1732762754 270360576 57861 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 66006 57861 145 145 0 65861 0
[pid=13387] vsize: 264024
Current children cumulated CPU time (s) 377.47
Current children cumulated vsize (Kb) 266148

[startup+390.036 s]
Raw data (loadavg): 1.01 1.09 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 59771 0 0 0 38485 260 0 0 25 0 1 0 1732762754 270606336 57922 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 66066 57922 145 145 0 65921 0
[pid=13387] vsize: 264264
Current children cumulated CPU time (s) 387.46
Current children cumulated vsize (Kb) 266388

[startup+400.037 s]
Raw data (loadavg): 1.01 1.09 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 59831 0 0 0 39485 261 0 0 25 0 1 0 1732762754 270852096 57982 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 66126 57982 145 145 0 65981 0
[pid=13387] vsize: 264504
Current children cumulated CPU time (s) 397.47
Current children cumulated vsize (Kb) 266628

[startup+410.038 s]
Raw data (loadavg): 1.00 1.09 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 59900 0 0 0 40484 261 0 0 25 0 1 0 1732762754 271130624 58051 4294967295 134512640 135094434 3221224432 3221223024 134557528 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 66194 58051 145 145 0 66049 0
[pid=13387] vsize: 264776
Current children cumulated CPU time (s) 407.46
Current children cumulated vsize (Kb) 266900

[startup+420.037 s]
Raw data (loadavg): 1.00 1.08 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 59957 0 0 0 41483 262 0 0 25 0 1 0 1732762754 271364096 58108 4294967295 134512640 135094434 3221224432 3221223024 134556914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 66251 58108 145 145 0 66106 0
[pid=13387] vsize: 265004
Current children cumulated CPU time (s) 417.46
Current children cumulated vsize (Kb) 267128

[startup+430.038 s]
Raw data (loadavg): 1.00 1.08 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 60021 0 0 0 42482 262 0 0 25 0 1 0 1732762754 271626240 58172 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 66315 58172 145 145 0 66170 0
[pid=13387] vsize: 265260
Current children cumulated CPU time (s) 427.45
Current children cumulated vsize (Kb) 267384

[startup+440.038 s]
Raw data (loadavg): 1.00 1.08 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 60089 0 0 0 43481 263 0 0 25 0 1 0 1732762754 271900672 58240 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 66382 58240 145 145 0 66237 0
[pid=13387] vsize: 265528
Current children cumulated CPU time (s) 437.45
Current children cumulated vsize (Kb) 267652

[startup+450.038 s]
Raw data (loadavg): 1.00 1.07 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 60191 0 0 0 44479 265 0 0 25 0 1 0 1732762754 272318464 58342 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 66484 58342 145 145 0 66339 0
[pid=13387] vsize: 265936
Current children cumulated CPU time (s) 447.45
Current children cumulated vsize (Kb) 268060

[startup+460.041 s]
Raw data (loadavg): 1.08 1.09 1.01 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 60252 0 0 0 45478 266 0 0 25 0 1 0 1732762754 272568320 58403 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 66545 58403 145 145 0 66400 0
[pid=13387] vsize: 266180
Current children cumulated CPU time (s) 457.45
Current children cumulated vsize (Kb) 268304

[startup+470.041 s]
Raw data (loadavg): 1.07 1.08 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 60324 0 0 0 46477 266 0 0 25 0 1 0 1732762754 272863232 58475 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 66617 58475 145 145 0 66472 0
[pid=13387] vsize: 266468
Current children cumulated CPU time (s) 467.44
Current children cumulated vsize (Kb) 268592

[startup+480.041 s]
Raw data (loadavg): 1.06 1.08 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 60395 0 0 0 47476 267 0 0 25 0 1 0 1732762754 273149952 58546 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 66687 58546 145 145 0 66542 0
[pid=13387] vsize: 266748
Current children cumulated CPU time (s) 477.44
Current children cumulated vsize (Kb) 268872

[startup+490.041 s]
Raw data (loadavg): 1.05 1.08 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 60513 0 0 0 48475 268 0 0 25 0 1 0 1732762754 273629184 58664 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 66804 58664 145 145 0 66659 0
[pid=13387] vsize: 267216
Current children cumulated CPU time (s) 487.44
Current children cumulated vsize (Kb) 269340

[startup+500.043 s]
Raw data (loadavg): 1.04 1.08 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 60613 0 0 0 49474 268 0 0 25 0 1 0 1732762754 274038784 58764 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 66904 58764 145 145 0 66759 0
[pid=13387] vsize: 267616
Current children cumulated CPU time (s) 497.43
Current children cumulated vsize (Kb) 269740

[startup+510.043 s]
Raw data (loadavg): 1.03 1.07 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 60689 0 0 0 50473 269 0 0 25 0 1 0 1732762754 274350080 58840 4294967295 134512640 135094434 3221224432 3221223024 134556941 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 66980 58840 145 145 0 66835 0
[pid=13387] vsize: 267920
Current children cumulated CPU time (s) 507.43
Current children cumulated vsize (Kb) 270044

[startup+520.044 s]
Raw data (loadavg): 1.03 1.07 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 60780 0 0 0 51472 270 0 0 25 0 1 0 1732762754 274784256 58931 4294967295 134512640 135094434 3221224432 3221223044 134563089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 67086 58931 145 145 0 66941 0
[pid=13387] vsize: 268344
Current children cumulated CPU time (s) 517.43
Current children cumulated vsize (Kb) 270468

[startup+530.045 s]
Raw data (loadavg): 1.02 1.07 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 60871 0 0 0 52470 271 0 0 25 0 1 0 1732762754 275161088 59022 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 67178 59022 145 145 0 67033 0
[pid=13387] vsize: 268712
Current children cumulated CPU time (s) 527.42
Current children cumulated vsize (Kb) 270836

[startup+540.044 s]
Raw data (loadavg): 1.02 1.06 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 60966 0 0 0 53469 272 0 0 25 0 1 0 1732762754 275542016 59117 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13387/statm): 67271 59117 145 145 0 67126 0
[pid=13387] vsize: 269084
Current children cumulated CPU time (s) 537.42
Current children cumulated vsize (Kb) 271208

[startup+550.045 s]
Raw data (loadavg): 1.02 1.06 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 61038 0 0 0 54468 272 0 0 25 0 1 0 1732762754 275836928 59189 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 67343 59189 145 145 0 67198 0
[pid=13387] vsize: 269372
Current children cumulated CPU time (s) 547.41
Current children cumulated vsize (Kb) 271496

[startup+560.046 s]
Raw data (loadavg): 1.01 1.06 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 61105 0 0 0 55466 273 0 0 25 0 1 0 1732762754 276107264 59256 4294967295 134512640 135094434 3221224432 3221223088 134561688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 67409 59256 145 145 0 67264 0
[pid=13387] vsize: 269636
Current children cumulated CPU time (s) 557.4
Current children cumulated vsize (Kb) 271760

[startup+570.045 s]
Raw data (loadavg): 1.01 1.06 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 61151 0 0 0 56466 273 0 0 25 0 1 0 1732762754 276295680 59302 4294967295 134512640 135094434 3221224432 3221223072 134558269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 67455 59302 145 145 0 67310 0
[pid=13387] vsize: 269820
Current children cumulated CPU time (s) 567.4
Current children cumulated vsize (Kb) 271944

[startup+580.046 s]
Raw data (loadavg): 1.01 1.05 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 61216 0 0 0 57464 274 0 0 25 0 1 0 1732762754 276561920 59367 4294967295 134512640 135094434 3221224432 3221223056 134562139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 67520 59367 145 145 0 67375 0
[pid=13387] vsize: 270080
Current children cumulated CPU time (s) 577.39
Current children cumulated vsize (Kb) 272204

[startup+590.047 s]
Raw data (loadavg): 1.01 1.05 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 61279 0 0 0 58464 275 0 0 25 0 1 0 1732762754 276815872 59430 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 67582 59430 145 145 0 67437 0
[pid=13387] vsize: 270328
Current children cumulated CPU time (s) 587.4
Current children cumulated vsize (Kb) 272452

[startup+600.048 s]
Raw data (loadavg): 1.00 1.05 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 61380 0 0 0 59463 275 0 0 25 0 1 0 1732762754 277229568 59531 4294967295 134512640 135094434 3221224432 3221223024 134556866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 67683 59531 145 145 0 67538 0
[pid=13387] vsize: 270732
Current children cumulated CPU time (s) 597.39
Current children cumulated vsize (Kb) 272856

[startup+610.048 s]
Raw data (loadavg): 1.00 1.05 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 61457 0 0 0 60462 275 0 0 25 0 1 0 1732762754 277544960 59608 4294967295 134512640 135094434 3221224432 3221223044 134563104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 67760 59608 145 145 0 67615 0
[pid=13387] vsize: 271040
Current children cumulated CPU time (s) 607.38
Current children cumulated vsize (Kb) 273164

[startup+620.048 s]
Raw data (loadavg): 1.00 1.05 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 61540 0 0 0 61461 276 0 0 25 0 1 0 1732762754 277880832 59691 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 67842 59691 145 145 0 67697 0
[pid=13387] vsize: 271368
Current children cumulated CPU time (s) 617.38
Current children cumulated vsize (Kb) 273492

[startup+630.049 s]
Raw data (loadavg): 1.00 1.04 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 61624 0 0 0 62460 276 0 0 25 0 1 0 1732762754 278224896 59775 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 67926 59775 145 145 0 67781 0
[pid=13387] vsize: 271704
Current children cumulated CPU time (s) 627.37
Current children cumulated vsize (Kb) 273828

[startup+640.049 s]
Raw data (loadavg): 1.00 1.04 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 61717 0 0 0 63459 277 0 0 25 0 1 0 1732762754 278605824 59868 4294967295 134512640 135094434 3221224432 3221223024 134556834 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 68019 59868 145 145 0 67874 0
[pid=13387] vsize: 272076
Current children cumulated CPU time (s) 637.37
Current children cumulated vsize (Kb) 274200

[startup+650.05 s]
Raw data (loadavg): 1.00 1.04 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 61852 0 0 0 64457 277 0 0 25 0 1 0 1732762754 279158784 60003 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 68154 60003 145 145 0 68009 0
[pid=13387] vsize: 272616
Current children cumulated CPU time (s) 647.35
Current children cumulated vsize (Kb) 274740

[startup+660.051 s]
Raw data (loadavg): 1.00 1.04 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 61937 0 0 0 65456 278 0 0 25 0 1 0 1732762754 279515136 60088 4294967295 134512640 135094434 3221224432 3221223024 134557037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 68241 60088 145 145 0 68096 0
[pid=13387] vsize: 272964
Current children cumulated CPU time (s) 657.35
Current children cumulated vsize (Kb) 275088

[startup+670.05 s]
Raw data (loadavg): 1.00 1.04 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 62019 0 0 0 66455 278 0 0 25 0 1 0 1732762754 279830528 60170 4294967295 134512640 135094434 3221224432 3221223044 134563059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 68318 60170 145 145 0 68173 0
[pid=13387] vsize: 273272
Current children cumulated CPU time (s) 667.34
Current children cumulated vsize (Kb) 275396

[startup+680.051 s]
Raw data (loadavg): 1.00 1.04 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 62113 0 0 0 67453 279 0 0 25 0 1 0 1732762754 280215552 60264 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 68412 60264 145 145 0 68267 0
[pid=13387] vsize: 273648
Current children cumulated CPU time (s) 677.33
Current children cumulated vsize (Kb) 275772

[startup+690.052 s]
Raw data (loadavg): 1.00 1.03 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 62192 0 0 0 68452 280 0 0 25 0 1 0 1732762754 280535040 60343 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 68490 60343 145 145 0 68345 0
[pid=13387] vsize: 273960
Current children cumulated CPU time (s) 687.33
Current children cumulated vsize (Kb) 276084

[startup+700.053 s]
Raw data (loadavg): 1.00 1.03 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 62253 0 0 0 69452 280 0 0 25 0 1 0 1732762754 280784896 60404 4294967295 134512640 135094434 3221224432 3221223024 134557016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 68551 60404 145 145 0 68406 0
[pid=13387] vsize: 274204
Current children cumulated CPU time (s) 697.33
Current children cumulated vsize (Kb) 276328

[startup+710.054 s]
Raw data (loadavg): 1.00 1.03 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 62307 0 0 0 70451 280 0 0 25 0 1 0 1732762754 281006080 60458 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 68605 60458 145 145 0 68460 0
[pid=13387] vsize: 274420
Current children cumulated CPU time (s) 707.32
Current children cumulated vsize (Kb) 276544

[startup+720.054 s]
Raw data (loadavg): 1.00 1.03 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 62380 0 0 0 71451 281 0 0 25 0 1 0 1732762754 281300992 60531 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 68677 60531 145 145 0 68532 0
[pid=13387] vsize: 274708
Current children cumulated CPU time (s) 717.33
Current children cumulated vsize (Kb) 276832

[startup+730.054 s]
Raw data (loadavg): 1.00 1.03 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 62471 0 0 0 72450 281 0 0 25 0 1 0 1732762754 281673728 60622 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 68768 60622 145 145 0 68623 0
[pid=13387] vsize: 275072
Current children cumulated CPU time (s) 727.32
Current children cumulated vsize (Kb) 277196

[startup+740.055 s]
Raw data (loadavg): 1.00 1.03 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 62552 0 0 0 73449 282 0 0 25 0 1 0 1732762754 282005504 60703 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 68849 60703 145 145 0 68704 0
[pid=13387] vsize: 275396
Current children cumulated CPU time (s) 737.32
Current children cumulated vsize (Kb) 277520

[startup+750.056 s]
Raw data (loadavg): 1.00 1.03 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 62614 0 0 0 74448 282 0 0 25 0 1 0 1732762754 282255360 60765 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 68910 60765 145 145 0 68765 0
[pid=13387] vsize: 275640
Current children cumulated CPU time (s) 747.31
Current children cumulated vsize (Kb) 277764

[startup+760.056 s]
Raw data (loadavg): 1.00 1.02 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 62692 0 0 0 75446 283 0 0 25 0 1 0 1732762754 282574848 60843 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 68988 60843 145 145 0 68843 0
[pid=13387] vsize: 275952
Current children cumulated CPU time (s) 757.3
Current children cumulated vsize (Kb) 278076

[startup+770.056 s]
Raw data (loadavg): 1.00 1.02 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 62810 0 0 0 76445 284 0 0 25 0 1 0 1732762754 283058176 60961 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 69106 60961 145 145 0 68961 0
[pid=13387] vsize: 276424
Current children cumulated CPU time (s) 767.3
Current children cumulated vsize (Kb) 278548

[startup+780.057 s]
Raw data (loadavg): 1.00 1.02 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 62876 0 0 0 77443 284 0 0 25 0 1 0 1732762754 283324416 61027 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 69171 61027 145 145 0 69026 0
[pid=13387] vsize: 276684
Current children cumulated CPU time (s) 777.28
Current children cumulated vsize (Kb) 278808

[startup+790.058 s]
Raw data (loadavg): 1.00 1.02 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 62965 0 0 0 78442 285 0 0 25 0 1 0 1732762754 283697152 61116 4294967295 134512640 135094434 3221224432 3221223024 134556931 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 69262 61116 145 145 0 69117 0
[pid=13387] vsize: 277048
Current children cumulated CPU time (s) 787.28
Current children cumulated vsize (Kb) 279172

[startup+800.058 s]
Raw data (loadavg): 1.00 1.02 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 63026 0 0 0 79441 286 0 0 25 0 1 0 1732762754 283938816 61177 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13387/statm): 69321 61177 145 145 0 69176 0
[pid=13387] vsize: 277284
Current children cumulated CPU time (s) 797.28
Current children cumulated vsize (Kb) 279408

[startup+810.059 s]
Raw data (loadavg): 1.00 1.02 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 63103 0 0 0 80440 287 0 0 25 0 1 0 1732762754 284258304 61254 4294967295 134512640 135094434 3221224432 3221223024 134556809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 69399 61254 145 145 0 69254 0
[pid=13387] vsize: 277596
Current children cumulated CPU time (s) 807.28
Current children cumulated vsize (Kb) 279720

[startup+820.06 s]
Raw data (loadavg): 1.00 1.02 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 63172 0 0 0 81439 287 0 0 25 0 1 0 1732762754 284532736 61323 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 69466 61323 145 145 0 69321 0
[pid=13387] vsize: 277864
Current children cumulated CPU time (s) 817.27
Current children cumulated vsize (Kb) 279988

[startup+830.06 s]
Raw data (loadavg): 1.00 1.02 1.00 1/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) T 13383 13383 20602 0 -1 0 63261 0 0 0 82438 288 0 0 25 0 1 0 1732762754 284897280 61412 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/13387/statm): 69555 61412 145 145 0 69410 0
[pid=13387] vsize: 278220
Current children cumulated CPU time (s) 827.27
Current children cumulated vsize (Kb) 280344

[startup+840.06 s]
Raw data (loadavg): 1.00 1.02 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 63342 0 0 0 83437 288 0 0 25 0 1 0 1732762754 285224960 61493 4294967295 134512640 135094434 3221224432 3221223120 134554687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 69635 61493 145 145 0 69490 0
[pid=13387] vsize: 278540
Current children cumulated CPU time (s) 837.26
Current children cumulated vsize (Kb) 280664

[startup+850.061 s]
Raw data (loadavg): 1.00 1.02 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 63453 0 0 0 84435 289 0 0 25 0 1 0 1732762754 285679616 61604 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 69746 61604 145 145 0 69601 0
[pid=13387] vsize: 278984
Current children cumulated CPU time (s) 847.25
Current children cumulated vsize (Kb) 281108

[startup+860.061 s]
Raw data (loadavg): 1.00 1.01 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 63515 0 0 0 85434 290 0 0 25 0 1 0 1732762754 285933568 61666 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 69808 61666 145 145 0 69663 0
[pid=13387] vsize: 279232
Current children cumulated CPU time (s) 857.25
Current children cumulated vsize (Kb) 281356

[startup+870.061 s]
Raw data (loadavg): 1.00 1.01 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 63581 0 0 0 86433 290 0 0 25 0 1 0 1732762754 286199808 61732 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 69873 61732 145 145 0 69728 0
[pid=13387] vsize: 279492
Current children cumulated CPU time (s) 867.24
Current children cumulated vsize (Kb) 281616

[startup+880.062 s]
Raw data (loadavg): 1.00 1.01 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 63646 0 0 0 87431 291 0 0 25 0 1 0 1732762754 286466048 61797 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 69938 61797 145 145 0 69793 0
[pid=13387] vsize: 279752
Current children cumulated CPU time (s) 877.23
Current children cumulated vsize (Kb) 281876

[startup+890.061 s]
Raw data (loadavg): 1.00 1.01 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 63706 0 0 0 88430 291 0 0 25 0 1 0 1732762754 286711808 61857 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 69998 61857 145 145 0 69853 0
[pid=13387] vsize: 279992
Current children cumulated CPU time (s) 887.22
Current children cumulated vsize (Kb) 282116

[startup+900.062 s]
Raw data (loadavg): 1.00 1.01 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 63775 0 0 0 89429 292 0 0 25 0 1 0 1732762754 286990336 61926 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 70066 61926 145 145 0 69921 0
[pid=13387] vsize: 280264
Current children cumulated CPU time (s) 897.22
Current children cumulated vsize (Kb) 282388

[startup+910.063 s]
Raw data (loadavg): 1.00 1.01 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 63846 0 0 0 90428 292 0 0 25 0 1 0 1732762754 287281152 61997 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 70137 61997 145 145 0 69992 0
[pid=13387] vsize: 280548
Current children cumulated CPU time (s) 907.21
Current children cumulated vsize (Kb) 282672

[startup+920.062 s]
Raw data (loadavg): 1.00 1.01 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 63914 0 0 0 91427 293 0 0 25 0 1 0 1732762754 287559680 62065 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 70205 62065 145 145 0 70060 0
[pid=13387] vsize: 280820
Current children cumulated CPU time (s) 917.21
Current children cumulated vsize (Kb) 282944

[startup+930.063 s]
Raw data (loadavg): 1.00 1.01 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 63991 0 0 0 92426 294 0 0 25 0 1 0 1732762754 287875072 62142 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 70282 62142 145 145 0 70137 0
[pid=13387] vsize: 281128
Current children cumulated CPU time (s) 927.21
Current children cumulated vsize (Kb) 283252

[startup+940.064 s]
Raw data (loadavg): 1.00 1.01 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 64074 0 0 0 93425 294 0 0 25 0 1 0 1732762754 288210944 62225 4294967295 134512640 135094434 3221224432 3221223072 134558269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 70364 62225 145 145 0 70219 0
[pid=13387] vsize: 281456
Current children cumulated CPU time (s) 937.2
Current children cumulated vsize (Kb) 283580

[startup+950.064 s]
Raw data (loadavg): 1.00 1.01 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 64175 0 0 0 94424 295 0 0 25 0 1 0 1732762754 288624640 62326 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 70465 62326 145 145 0 70320 0
[pid=13387] vsize: 281860
Current children cumulated CPU time (s) 947.2
Current children cumulated vsize (Kb) 283984

[startup+960.065 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 64259 0 0 0 95423 295 0 0 25 0 1 0 1732762754 288968704 62410 4294967295 134512640 135094434 3221224432 3221223044 134563092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 70549 62410 145 145 0 70404 0
[pid=13387] vsize: 282196
Current children cumulated CPU time (s) 957.19
Current children cumulated vsize (Kb) 284320

[startup+970.066 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 64391 0 0 0 96422 296 0 0 25 0 1 0 1732762754 289509376 62542 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 70681 62542 145 145 0 70536 0
[pid=13387] vsize: 282724
Current children cumulated CPU time (s) 967.19
Current children cumulated vsize (Kb) 284848

[startup+980.067 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 64478 0 0 0 97421 296 0 0 25 0 1 0 1732762754 289861632 62629 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 70767 62629 145 145 0 70622 0
[pid=13387] vsize: 283068
Current children cumulated CPU time (s) 977.18
Current children cumulated vsize (Kb) 285192

[startup+990.066 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 64554 0 0 0 98420 297 0 0 25 0 1 0 1732762754 290172928 62705 4294967295 134512640 135094434 3221224432 3221223088 134558420 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 70843 62705 145 145 0 70698 0
[pid=13387] vsize: 283372
Current children cumulated CPU time (s) 987.18
Current children cumulated vsize (Kb) 285496

[startup+1000.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 64640 0 0 0 99419 297 0 0 25 0 1 0 1732762754 290525184 62791 4294967295 134512640 135094434 3221224432 3221223088 134558276 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 70929 62791 145 145 0 70784 0
[pid=13387] vsize: 283716
Current children cumulated CPU time (s) 997.17
Current children cumulated vsize (Kb) 285840

[startup+1010.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 64722 0 0 0 100418 298 0 0 25 0 1 0 1732762754 290861056 62873 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 71011 62873 145 145 0 70866 0
[pid=13387] vsize: 284044
Current children cumulated CPU time (s) 1007.17
Current children cumulated vsize (Kb) 286168

[startup+1020.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 64848 0 0 0 101416 299 0 0 25 0 1 0 1732762754 291504128 62999 4294967295 134512640 135094434 3221224432 3221223120 134554717 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 71168 62999 145 145 0 71023 0
[pid=13387] vsize: 284672
Current children cumulated CPU time (s) 1017.16
Current children cumulated vsize (Kb) 286796

[startup+1030.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 64900 0 0 0 102416 300 0 0 25 0 1 0 1732762754 291717120 63051 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 71220 63051 145 145 0 71075 0
[pid=13387] vsize: 284880
Current children cumulated CPU time (s) 1027.17
Current children cumulated vsize (Kb) 287004

[startup+1040.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 64983 0 0 0 103415 300 0 0 25 0 1 0 1732762754 292061184 63134 4294967295 134512640 135094434 3221224432 3221223056 134562128 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 71304 63134 145 145 0 71159 0
[pid=13387] vsize: 285216
Current children cumulated CPU time (s) 1037.16
Current children cumulated vsize (Kb) 287340

[startup+1050.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 65058 0 0 0 104414 302 0 0 25 0 1 0 1732762754 292364288 63209 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 71378 63209 145 145 0 71233 0
[pid=13387] vsize: 285512
Current children cumulated CPU time (s) 1047.17
Current children cumulated vsize (Kb) 287636

[startup+1060.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 65125 0 0 0 105413 302 0 0 25 0 1 0 1732762754 292634624 63276 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 71444 63276 145 145 0 71299 0
[pid=13387] vsize: 285776
Current children cumulated CPU time (s) 1057.16
Current children cumulated vsize (Kb) 287900

[startup+1070.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 65237 0 0 0 106412 303 0 0 25 0 1 0 1732762754 293093376 63388 4294967295 134512640 135094434 3221224432 3221223024 134556999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 71556 63388 145 145 0 71411 0
[pid=13387] vsize: 286224
Current children cumulated CPU time (s) 1067.16
Current children cumulated vsize (Kb) 288348

[startup+1080.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 65307 0 0 0 107411 304 0 0 25 0 1 0 1732762754 293380096 63458 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 71626 63458 145 145 0 71481 0
[pid=13387] vsize: 286504
Current children cumulated CPU time (s) 1077.16
Current children cumulated vsize (Kb) 288628

[startup+1090.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 65378 0 0 0 108410 304 0 0 25 0 1 0 1732762754 293666816 63529 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 71696 63529 145 145 0 71551 0
[pid=13387] vsize: 286784
Current children cumulated CPU time (s) 1087.15
Current children cumulated vsize (Kb) 288908

[startup+1100.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 65438 0 0 0 109408 305 0 0 25 0 1 0 1732762754 293912576 63589 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 71756 63589 145 145 0 71611 0
[pid=13387] vsize: 287024
Current children cumulated CPU time (s) 1097.14
Current children cumulated vsize (Kb) 289148

[startup+1110.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 65508 0 0 0 110407 306 0 0 25 0 1 0 1732762754 294199296 63659 4294967295 134512640 135094434 3221224432 3221223044 134563087 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 71826 63659 145 145 0 71681 0
[pid=13387] vsize: 287304
Current children cumulated CPU time (s) 1107.14
Current children cumulated vsize (Kb) 289428

[startup+1120.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 65584 0 0 0 111407 306 0 0 25 0 1 0 1732762754 294506496 63735 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 71901 63735 145 145 0 71756 0
[pid=13387] vsize: 287604
Current children cumulated CPU time (s) 1117.14
Current children cumulated vsize (Kb) 289728

[startup+1130.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 65670 0 0 0 112405 307 0 0 25 0 1 0 1732762754 294858752 63821 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 71987 63821 145 145 0 71842 0
[pid=13387] vsize: 287948
Current children cumulated CPU time (s) 1127.13
Current children cumulated vsize (Kb) 290072

[startup+1140.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 65746 0 0 0 113405 308 0 0 25 0 1 0 1732762754 295170048 63897 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 72063 63897 145 145 0 71918 0
[pid=13387] vsize: 288252
Current children cumulated CPU time (s) 1137.14
Current children cumulated vsize (Kb) 290376

[startup+1150.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 65840 0 0 0 114404 309 0 0 25 0 1 0 1732762754 295550976 63991 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 72156 63991 145 145 0 72011 0
[pid=13387] vsize: 288624
Current children cumulated CPU time (s) 1147.14
Current children cumulated vsize (Kb) 290748

[startup+1160.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 65935 0 0 0 115403 310 0 0 25 0 1 0 1732762754 295944192 64086 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 72252 64086 145 145 0 72107 0
[pid=13387] vsize: 289008
Current children cumulated CPU time (s) 1157.14
Current children cumulated vsize (Kb) 291132

[startup+1170.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 66010 0 0 0 116401 311 0 0 25 0 1 0 1732762754 296247296 64161 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 72326 64161 145 145 0 72181 0
[pid=13387] vsize: 289304
Current children cumulated CPU time (s) 1167.13
Current children cumulated vsize (Kb) 291428

[startup+1180.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 66088 0 0 0 117400 312 0 0 25 0 1 0 1732762754 296566784 64239 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 72404 64239 145 145 0 72259 0
[pid=13387] vsize: 289616
Current children cumulated CPU time (s) 1177.13
Current children cumulated vsize (Kb) 291740

[startup+1190.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 66164 0 0 0 118399 313 0 0 25 0 1 0 1732762754 296873984 64315 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 72479 64315 145 145 0 72334 0
[pid=13387] vsize: 289916
Current children cumulated CPU time (s) 1187.13
Current children cumulated vsize (Kb) 292040

[startup+1200.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 66288 0 0 0 119397 314 0 0 25 0 1 0 1732762754 297381888 64439 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 72603 64439 145 145 0 72458 0
[pid=13387] vsize: 290412
Current children cumulated CPU time (s) 1197.12
Current children cumulated vsize (Kb) 292536

[startup+1210.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 66365 0 0 0 120397 314 0 0 25 0 1 0 1732762754 297697280 64516 4294967295 134512640 135094434 3221224432 3221223024 134557002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 72680 64516 145 145 0 72535 0
[pid=13387] vsize: 290720
Current children cumulated CPU time (s) 1207.12
Current children cumulated vsize (Kb) 292844



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 13708
Raw data (/proc/13383/stat): 13383 (minisat+_script) S 13382 13383 20602 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1732762749 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13383/statm): 531 226 485 147 0 384 0
[pid=13383] vsize: 2124
Raw data (/proc/13387/stat): 13387 (minisat+_64-bit) R 13383 13383 20602 0 -1 0 66365 0 0 0 120397 314 0 0 25 0 1 0 1732762754 297697280 64516 4294967295 134512640 135094434 3221224432 3221223024 134556870 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13387/statm): 72680 64516 145 145 0 72535 0
[pid=13387] vsize: 290720
Current children cumulated CPU time (s) 1207.12
Current children cumulated vsize (Kb) 292844

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

Child status: 0
Real time (s): 1210.21
CPU time (s): 1207.24
CPU user time (s): 1203.97
CPU system time (s): 3.2685
CPU usage (%): 99.7547
Max. virtual memory (cumulated for all children) (Kb): 292844

Verifier Data

ERROR: no interpretation found !